Amal Ahmed (Northeastern University): Semantic Intermediate Representations for the Working Metatheoretician

Wednesday August 3, 2-3pm

Designers of typed programming languages commonly prove meta-theoretic properties such as type soundness for at least a core of their language. But any practical language implementation must provide some way of interoperating with code written in other languages -- usually via a foreign-function interface (FFI) -- which opens the door to new, potentially unsafe, behaviors that aren't accounted for in the original type soundness proof. Despite the prevalence of interoperability in practical software, principled foundations for the end-to-end design, implementation, and verification of interoperability mechanisms have been largely neglected. In this talk, I'll advocate a proof technique for _working metatheoreticians_ seeking to ensure soundness or security properties of real languages, which implement interoperability using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). This proof technique involves building a _semantic intermediate representation_: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. More interestingly, semantic IRs provide a basis for numerous avenues of future work on the principled design of language interoperability: how to support the inclusion of libraries whose behavior is foreign to the original language, how to prove soundness and security properties that are robust to behaviors (attackers) outside of the semantic IR, and how to develop a semantic-IR compiler backend that makes it easier to implement and verify sound interoperability for a wide array of source languages.

Miklaj Bojanczyk (University of Warsaw): Transducers of polynomial growth

Friday August 5, 9-10am

The polyregular functions are a class of string-to-string functions that have polynomial size outputs, and which can be defined using finite state models. There are many equivalent definitions of this class, with roots in automata theory, programming languages and logic. The talk surveys recent results on polyregular functions. It presents five of the equivalent definitions, and gives self-contained proofs for most of the equivalences. Decision problems as well as restricted subclasses of the polyregular functions are also discussed.

See also LICS Plenary and Keynote Talks.

• Elena Di Lavore, Giovanni de Felice and Mario Román. Monoidal Streams for Dataflow Programming.
• Jakub Gajarsky, Michal Pilipczuk and Szymon Torunczyk. Stable graphs of bounded twin-width.
• Edon Kelmendi. Computing the Density of the Positivity Set for Linear Recurrence Sequences.
• Moritz Lichter and Pascal Schweitzer. Choiceless Polynomial Time with Witnessed Symmetric Choice.
• Junyi Liu, Li Zhou, Gilles Barthe and Mingsheng Ying. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.
• Thomas Place. The amazing mixed polynomial closure and its applications to two- variable first-order logic.

• Elena Di Lavore, Giovanni de Felice and Mario Román. Monoidal Streams for Dataflow Programming.
• Yoàv Montacute and Nihil Shah. The Pebble-Relation Comonad in Finite Model Theory.