BEGIN:VCALENDAR
CALSCALE:GREGORIAN
PRODID:-//Ximian//NONSGML Evolution Calendar//EN
VERSION:2.0
BEGIN:VTIMEZONE
TZID:/freeassociation.sourceforge.net/Europe/Lisbon
X-LIC-LOCATION:Europe/Lisbon
BEGIN:STANDARD
TZNAME:LMT
TZOFFSETFROM:-003645
TZOFFSETTO:-003645
DTSTART:18840101T000000
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:-003645
TZOFFSETTO:+0000
DTSTART:19111231T232315
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19160617T230000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19161101T010000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19170301T000000
RRULE:FREQ=YEARLY;UNTIL=19210301T000000Z;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19171015T000000
RRULE:FREQ=YEARLY;UNTIL=19211014T230000Z;BYDAY=SA;BYMONTHDAY=15;
 BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19240416T230000
RDATE:19260417T230000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19241005T000000
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19261003T000000
RRULE:FREQ=YEARLY;UNTIL=19291005T230000Z;BYDAY=1SU;BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19270409T230000
RRULE:FREQ=YEARLY;UNTIL=19280414T230000Z;BYDAY=2SA;BYMONTH=4
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19290420T230000
RDATE:19310418T230000
RDATE:19320402T230000
RDATE:19340407T230000
RDATE:19350330T230000
RDATE:19360418T230000
RDATE:19370403T230000
RDATE:19380326T230000
RDATE:19390415T230000
RDATE:19400224T230000
RDATE:19410405T230000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19311004T000000
RRULE:FREQ=YEARLY;UNTIL=19321001T230000Z;BYDAY=1SU;BYMONTH=10
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19341007T000000
RRULE:FREQ=YEARLY;UNTIL=19381001T230000Z;BYDAY=1SU;BYMONTH=10
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19391119T000000
RDATE:19401008T000000
RDATE:19411006T000000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19420314T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEMT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19420425T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19420816T000000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19421025T000000
RRULE:FREQ=YEARLY;UNTIL=19451027T230000Z;BYDAY=-1SU;BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19430313T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEMT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19430417T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19430829T000000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19440311T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEMT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19440422T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19440827T000000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19450310T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEMT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19450421T230000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19450826T000000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19460406T230000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19461006T000000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19470406T020000
RRULE:FREQ=YEARLY;UNTIL=19660403T020000Z;BYDAY=1SU;BYMONTH=4
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19471005T030000
RRULE:FREQ=YEARLY;UNTIL=19651003T020000Z;BYDAY=1SU;BYMONTH=10
END:STANDARD
BEGIN:STANDARD
TZNAME:CET
TZOFFSETFROM:+0100
TZOFFSETTO:+0100
DTSTART:19661002T030000
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19760926T010000
RRULE:FREQ=YEARLY;UNTIL=19770925T000000Z;BYDAY=-1SU;BYMONTH=9
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19770327T000000
END:DAYLIGHT
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19780402T010000
RRULE:FREQ=YEARLY;UNTIL=19800406T010000Z;BYDAY=1SU;BYMONTH=4
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19781001T020000
END:STANDARD
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19790930T020000
RRULE:FREQ=YEARLY;UNTIL=19800928T010000Z;BYDAY=-1SU;BYMONTH=9
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19810329T000000
RRULE:FREQ=YEARLY;UNTIL=19850331T000000Z;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19810927T010000
RRULE:FREQ=YEARLY;UNTIL=19850929T000000Z;BYDAY=-1SU;BYMONTH=9
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19860330T010000
RRULE:FREQ=YEARLY;UNTIL=19920329T010000Z;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19860928T020000
RRULE:FREQ=YEARLY;UNTIL=19910929T010000Z;BYDAY=-1SU;BYMONTH=9
END:STANDARD
BEGIN:STANDARD
TZNAME:CET
TZOFFSETFROM:+0100
TZOFFSETTO:+0100
DTSTART:19920927T020000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19930328T020000
RRULE:FREQ=YEARLY;UNTIL=19950326T010000Z;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19930926T030000
RRULE:FREQ=YEARLY;UNTIL=19950924T010000Z;BYDAY=-1SU;BYMONTH=9
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0100
DTSTART:19960331T020000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:19961027T020000
RRULE:FREQ=YEARLY;UNTIL=20361026T010000Z;BYDAY=-1SU;BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:19970330T010000
RRULE:FREQ=YEARLY;UNTIL=20370329T010000Z;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:WET
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
DTSTART:20371025T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:WEST
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
DTSTART:20380328T010000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:1338b03ecd6ed2d724c5eff6f7d6afbc20083f8f
DTSTAMP:20260707T120853Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260716T090000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260716T093000
SUMMARY:Proof-Theoretic Compilation
SEQUENCE:8
CREATED:20260707T120914Z
LAST-MODIFIED:20260707T122129Z
RRULE;X-EVOLUTION-ENDDATE=20260717T080000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Frank Pfenning: https:
 //lcaires.github.io/fopps2026/pfenning.html\n\nWe know that 
 intuitionistic logic stands in the Curry-Howard correspondence with 
 functional computation.  Curry demonstrated this for an axioms and 
 combinatory reduction\, and Howard for natural deduction and the 
 lambda-calculus. What about other presentations of intuitionistic logic\, 
 such as the sequent calculus?  We introduce the semi-axiomatic sequent 
 calculus and show that it corresponds to functional computation with an 
 explicit store.  We further show how the subformula property induces data 
 layout\, and how translations between different inference systems can 
 form the core of a compiler.
END:VEVENT
BEGIN:VEVENT
UID:d3e40e4ba424163b357f818f5fbfdd67a92de7e0
DTSTAMP:20260707T120707Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T140000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T143000
SUMMARY:Effects and Handlers
SEQUENCE:10
CREATED:20260707T120734Z
LAST-MODIFIED:20260707T122044Z
RRULE;X-EVOLUTION-ENDDATE=20260716T130000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Sam Lindley: https:
 //lcaires.github.io/fopps2026/lindley.html\n\nEffect handlers allow 
 programmers to define\, customise\, and compose a range of crucial 
 programming features ranging from exceptions to lightweight threads to 
 probability\, inside the programming language. In this course I will give 
 a high-level introduction to the theory of algebraic effects and effect 
 handlers\, effect type systems for effect handlers\, and effect handler 
 oriented programming.
END:VEVENT
BEGIN:VEVENT
UID:5a8c3fe32f84effca2cf76e6e98db2b878e727c8
DTSTAMP:20260707T121618Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T173000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T183000
SUMMARY:Social Dinner
SEQUENCE:5
CREATED:20260707T121618Z
LAST-MODIFIED:20260707T122103Z
END:VEVENT
BEGIN:VEVENT
UID:2c60add91456c889aa0a9b5bf6dce839fa4aa956
DTSTAMP:20260707T115650Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T140000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T153000
SUMMARY:Program Verification Using Concurrent Separation Logic
SEQUENCE:14
CREATED:20260707T115739Z
LAST-MODIFIED:20260707T121943Z
RRULE;X-EVOLUTION-ENDDATE=20260714T130000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Robbert Krebbers: https:
 //lcaires.github.io/fopps2026/krebbers.html\n\nConcurrent programs are 
 challenging to get right\, especially if threads share access to memory. 
 The formalism of "Concurrent Separation Logic" (which was pioneered by 
 O'Hearn and Brookes in 2007) provides a powerful framework to verify 
 concurrent programs.\n\nOver the last 20 years\, concurrent separation 
 Logic has emerged into an active research field\, has been extended with 
 many features (e.g.\, fine-grained concurrency\, weak memory 
 consistency\, higher-order programs)\, been applied to many programming 
 languages (e.g.\, Rust)\, and has been implemented in numerous 
 verification tools (e.g.\, F*\, Iris\, Verifast\, Viper\, VST). We will 
 discuss the foundations of separation logic and show how they scale to 
 the verification of challenging concurrent programs. Exercises and demos 
 using the Iris framework in the Rocq proof assistant will be provided.
END:VEVENT
BEGIN:VEVENT
UID:c29fa75a495898704c47c51cf6d82b1afeb08106
DTSTAMP:20260707T120042Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T110000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T123000
SUMMARY:LiquidHaskell: Theorem Proving with Refinement Types
SEQUENCE:8
CREATED:20260707T120117Z
LAST-MODIFIED:20260707T122032Z
RRULE;X-EVOLUTION-ENDDATE=20260715T100000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Niki Vazou: https:
 //lcaires.github.io/fopps2026/vazou.html\n\nLiquid Haskell is an 
 extension to Haskell that adds refinement types to the language\, which 
 are then checked via an external theorem prover such as z3. With 
 refinement types\, one can express many interesting properties of 
 programs that are normally out of reach of Haskell's type system or only 
 achievable via quite substantial encoding efforts and advanced type 
 system constructs. On the other hand\, the overhead for checking 
 refinement types is often rather small\, because the external solver is 
 quite powerful.
END:VEVENT
BEGIN:VEVENT
UID:1691600b3006d8c53c11c582b37edaea9cc5081f
DTSTAMP:20260707T115947Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T090000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T103000
SUMMARY:Programming with Context-free Session Types
SEQUENCE:8
CREATED:20260707T120016Z
LAST-MODIFIED:20260707T122012Z
RRULE;X-EVOLUTION-ENDDATE=20260715T080000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Vasco T. Vasconcelos: https:
 //lcaires.github.io/fopps2026/vasconcelos.html\n\nSession types describe 
 protocols for concurrent message-passing programming. For many years 
 session types were realized as (possibly infinite) regular languages. 
 More recently\, context-free session types introduce a 
 sequential-composition type operator\, opening the doors to new classes 
 of protocols\, while promoting program modularity. Context-free session 
 types are now well-integrated with conventional type constructors\, 
 including functions\, records\, variants\, recursive\, universal and 
 existential constructors. There is however a price to pay for all this 
 flexibility: type equivalence becomes
END:VEVENT
BEGIN:VEVENT
UID:54c40134766337cefc9dfd0835ea8b5e68e1d5d0
DTSTAMP:20260707T121152Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260716T110000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260716T123000
SUMMARY:The LLM-Verifier Interface: Foundations for Soundness and 
 Effectiveness
SEQUENCE:10
RRULE;X-EVOLUTION-ENDDATE=20260717T100000Z:FREQ=DAILY;COUNT=2
CREATED:20260707T121227Z
LAST-MODIFIED:20260707T122145Z
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Nada Amin: https:
 //lcaires.github.io/fopps2026/amin.html\n\nLarge language models write 
 impressive code\, but can we trust it? Formal verification provides 
 mathematical guarantees\, but can it scale? This course explores how to 
 get both: generative systems that are sound (regardless of LLM behavior) 
 and effective through the LLM-verifier interface.                         
     \n\nWe examine how verification can contribute to these systems: not 
 just as a filter for correctness\, but as a source of feedback\, search 
 guidance\, and training signal. We look at what makes some architectures 
 succeed where others struggle\, including the granularity of generation\, 
 the structure of search\, and the role of partial verification. Examples 
 are drawn from neural theorem provers\, verified code generation\, and 
 specification synthesis.
END:VEVENT
BEGIN:VEVENT
UID:f48dc93fe67d6061ef4bcac70d1eaeb546820b62
DTSTAMP:20260707T115847Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T160000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T173000
SUMMARY:Formally Specifying ABIs Using Realistic Realizability
SEQUENCE:14
CREATED:20260707T115907Z
LAST-MODIFIED:20260707T122000Z
RRULE;X-EVOLUTION-ENDDATE=20260714T150000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Amal Ahmed: https:
 //lcaires.github.io/fopps2026/ahmed.html\n\nThe Application Binary 
 Interface (ABI) for a language specifies the interoperability rules for 
 each of its target platforms\, including properties such as data layout 
 and calling conventions. Compliance with these rules ensures “safe” 
 execution and may provide certain guarantees about resource usage. These 
 rules are relied upon by compilers for that language and others\, as well 
 as libraries and foreign-function interfaces. Unfortunately\, ABIs are 
 typically specified in prose and\, while type systems for source 
 languages have grown richer over time\, ABIs have largely remained the 
 same\, lacking analogous advances in expressivity and safety 
 guarantees.\n\nIn these lectures\, I’ll outline a vision for richer\, 
 semantic ABIs that would facilitate safer interoperability and library 
 integrations\, supported by a novel methodology for formally specifying 
 ABIs using realizability models. These semantic ABIs relate abstract\, 
 high-level types to unwieldy\, but well-behaved\, low-level code. I’ll 
 illustrate the approach with a case study\, showing how this methodology 
 leverages the last two decades of progress on separation logics and 
 semantic models. I’ll also discuss different practically-motivated ABI 
 design decisions and how they can be formalized via a semantic ABI\, 
 including a Swift-style ABI with library evolution. Finally\, I’ll 
 describe a new verified compiler backend we’re building to enable 
 easier specification of ABIs for the WebAssembly platform for high-level 
 languages in the future.
END:VEVENT
BEGIN:VEVENT
UID:f2264d1731e4a3aa6c29f72c0d8a395278aec828
DTSTAMP:20260707T120121Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T123000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260714T140000
SUMMARY:Lunch
SEQUENCE:9
CREATED:20260707T120134Z
LAST-MODIFIED:20260707T122115Z
RRULE:FREQ=DAILY;UNTIL=20260718T000000
END:VEVENT
BEGIN:VEVENT
UID:2b967ae6aced6010fecfa817095bb005e3ead685
DTSTAMP:20260707T115533Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T090000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260713T123000
SUMMARY:Registration
SEQUENCE:5
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
CREATED:20260707T115619Z
LAST-MODIFIED:20260707T121929Z
END:VEVENT
BEGIN:VEVENT
UID:76ee5612d5bab8a59fe9cb1e303aa41f691b67f7
DTSTAMP:20260707T120748Z
DTSTART;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T160000
DTEND;TZID=/freeassociation.sourceforge.net/Europe/Lisbon:
 20260715T173000
SUMMARY:Measuring and Enforcing Trust in Software and AI Systems
SEQUENCE:10
CREATED:20260707T120816Z
LAST-MODIFIED:20260707T122230Z
RRULE;X-EVOLUTION-ENDDATE=20260716T150000Z:FREQ=DAILY;COUNT=2
LOCATION:Edifício II - ISCTE\, Avenida das Forças Armadas\, 1649-026 
 Lisboa\, Portugal
DESCRIPTION:By Yuriy Brun: https:
 //lcaires.github.io/fopps2026/brun.html\n\nSoftware is ubiquitous and 
 trusting it is no longer optional. This course will start by exploring 
 what it means to trust software\, and how trust games\, a technique from 
 sociology and economics\, can help measure trust in software\, and 
 determine what factors affect that trust.  Next\, the course will 
 consider why systems that learn from data might be untrustworthy\, and 
 introduce Seldonian algorithms that fundamentally re-envision machine 
 learning to produce models that are probabilistically guaranteed to 
 satisfy fairness and safety requirements.  Finally\, the course will 
 explore how cutting-edge natural language processing techniques can 
 simplify formal verification\, increasing software trustworthiness.
END:VEVENT
END:VCALENDAR