Fri 20 Jan 2023 17:10 - 17:35 at Avenue34 - Semantics II Chair(s): Max S. New

Relational models of $\lambda$-calculus can be presented as type systems, the relational interpretation of a $\lambda$-term being given by the set of its typings. Within a distributors-induced bicategorical semantics generalizing the relational one, we identify the class of `categorified' graph models and show that they can be presented as type systems as well.
We prove that all the models living in this class satisfy an Approximation Theorem stating that the interpretation of a program corresponds to the filtered colimit of the denotations of its approximants. As in the relational case, the quantitative nature of our models allows to prove this property via a simple induction, rather than using impredicative techniques.
Unlike relational models, our 2-dimensional graph models are also proof-relevant in the sense that the interpretation of a $\lambda$-term does not contain only its typings, but the whole type derivations. The additional information carried by a type derivation permits to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterization of the theory induced by the categorified graph models as a simple corollary of the Approximation Theorem: two $\lambda$-terms have isomorphic interpretations exactly when their B"{o}hm trees coincide.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:45 - 18:00
Semantics IIPOPL at Avenue34
Chair(s): Max S. New University of Michigan
16:45
25m
Talk
Locally Nameless Sets
POPL
Andrew M. Pitts University of Cambridge
DOI Pre-print
17:10
25m
Talk
Why Are Proofs Relevant in Proof-Relevant Models?
POPL
Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds
DOI
17:35
25m
Talk
Towards a Higher-Order Mathematical Operational Semantics
POPL
Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg
DOI Pre-print