Welcome

Semantic Intermediate Representations for the Working Metatheoretician:

Abstract: 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.

Linear recurrences and Skolem problem (rescheduled talks from Tuesday)

Edon Kelmendi. Computing the Density of the Positivity Set for Linear Recurrence Sequences15 min

Richard Lipton, Florian Luca, Joris Nieuwveld, Joel Ouaknine, David Purser and James Worrell. On the Skolem Problem and the Skolem Conjecture15 min

Mario Roman. Monoidal Streams for Dataflow Programming

Paolo Pistone. Curry and Howard Meet Borel

Pascal Schweitzer. Choiceless Polynomial Time with Witnessed Symmetric Choice

Yoàv Montacute. The Pebble-Related Comonad in Finite Model Theory

Felipe Ferreira Santos. Separating LREC from LFP

Nikolas Mählmann. Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

LICS SC meeting (on invitation only)

pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)

Transducers of polynomial growth

Abstract: 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.

Daniel Gratzer. Normalization for multimodal type theory

Clemens Grabmayer. Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete

Soumodev Mal. On the Satisfiability of Context-free String Constraints with Subword Ordering

Matthias Naaf. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics

Jana Hofmann. Deciding Hyperproperties combined with Functional Specifications

Award Session: Kleene award, LICS Test-of-Time award, Church award