|
6th Summer
School on Foundations of Programming and Software Systems 13-17th July 2026 Emerging
Approaches for Reasoning about Programs and Proofs The 2026 Foundations of Programming and Software
Systems (FoPSS) Summer School brings together students and researchers to
explore "Emerging Approaches for Reasoning about Programs and
Proofs." This week-long school provides a broad and immersive
introduction to the latest developments on reasoning about programming. This
year’s edition is dedicated to recent methodologies, spanning advanced type
systems, proof assistants and logic, and neurosymbolic approaches, that are
actively shaping the frontier of software verification and program semantics. Our program features a distinguished series of
lectures designed to equip participants with both a solid grounding in
established foundations and a forward-looking perspective on the field's
future. By diving into highly active research areas, attendees will gain the
theoretical tools necessary to reason rigorously about complex, modern
programs. Through engaging instruction and collaborative discussions, the
school aims to inspire the next generation of researchers to push the
boundaries of what is possible in formal reasoning and program verification. |
The
series of Summer Schools on Foundations
of Programming and Software Systems (FoPSS) was jointly created by
EATCS, ETAPS, ACM SIGLOG and ACM SIGPLAN. The first FoPPS was organized in
2017. The goal
is to introduce the participants to various aspects of computation theory and
programming languages. The
school, spread over a single week, is aimed at students and researchers in
Theoretical Computer Science, broadly construed. Each year
the school is focused on a particular, actively researched topic. |
|
School of
Computer Science |
Proof-Theoretic
Compilation We 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. |
Attending
The 6
th FoPPS will be co-located with FLOC
2026 the 9th Federated Logic Conference, in the week prior to the
main conferences, and will take place in Lisbon, Portugal. Informations about
registration will be announced soon.
Planned Schedule
|
Mon |
Organizing Committee
Luís Caires, INESC ID and Técnico, University of Lisbon
José Fragoso, INESC ID and Técnico, University of Lisbon
Andreia Mordido, LASIGE and Ciências, University of
Lisbon
Bernardo Toninho, INESC ID and Técnico, University of
Lisbon