|
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
Engineering and Applied Sciences Harvard
University |
The
LLM-Verifier Interface: Large
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. We 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. |
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