Rencontre, 2 avril 2026

Programme

10:30 – 11:45

Mariangiola Dezani (Unviersità di Torino)

Invited talk: Intersection Type Galore

The first part of the talk reviews in full generality intersection type theories and filter models, i.e. lambda-calculus models, generated by them.

The second part of the talk gives an overview of how various authors exploited intersection types in different developments and applications.

Finally some new results dealing with the interpretation of unsolvable lambda-terms in filter models will be discussed.

13:45 – 14:45

Stephanie Weirich (University of Pennsylvania)

Invited talk: Tracking how dependently typed functions use their arguments

Dependent types increase the expressiveness of programming languages by allowing the result types of functions to depend on the values of their arguments. However, many of these arguments are purely specificational: they are there to provide information to the type checker, but otherwise have no runtime significance. Such arguments can be identified through various mechanisms, such as usage analysis (counting how many times functions use their parameters) or dependency analysis (tracking which results depend on which inputs).

In this talk, I will show how dependent type systems can integrate such analyses and make use of this information. In particular, I will provide an overview of the Dependent Calculus of Indistinguishability (DCOI), a system that uses dependency tracking to identify specificational arguments so that they may be erased at runtime and ignored during conversion.

This is joint work with Yiyun Liu, Jonathan Chan, and Jessica Shi.

15:15 – 16:15

Steve Zdancewic (University of Pennsylvania)

Invited talk: Vellvm: Formal Verification of LLVM IR Code

LLVM is an industrial-strength compiler that's used for everything from iOS development to academic research.  However, like any piece of complicated software, LLVM IR itself has a complex specification, making it hard to fully understand, and its implementation has bugs, which can cause potentially catastrophic mis-compilation errors. These properties make the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk will survey the Vellvm (Verified LLVM) project, which aims to define a formal, mathematical specification for a large, useful subset of LLVM.  Vellvm is implemented in the Rocq interactive theorem prover, which can be used for developing machine-checkable properties about LLVM IR programs and compiler optimization passes.  Along the way, we'll explore some subtleties of LLVM IR semantics and see how Vellvm models them in a modular way by composing "monadic interpreters" built on top of a data structure called _interaction trees_. We'll also see some applications of Vellvm for verified compiler construction.