|
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. |
|
Northeastern
University |
Formally Specifying ABIs Using
Realistic Realizability The
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. In 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. |
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