Laboratoire d'informatique de l'École polytechnique

Talk by Giulio Guerrieri: «Understanding the lambda-calculus via linearity and rewriting»

Speaker: Giulio Guerrieri
Location: Online
Date: Mon, 1 Mar 2021, 14:00-15:00

For the next seminar of the proofs and algorithms pole of LIX, we are happy to welcome Giulio Guerrieri, who will tell us about a unifying core language for studying lambda-calculi based on ideas from linear logic.

As usual, the seminar in the Monday slot will be followed by “virtual tea” in the Partout tea room which all are welcome to join.

Link to the online conference

Abstract: The lambda-calculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambda-calculi, depending on the evaluation mechanism (e.g., call-by-name, call-by-value, call-by-need) and computational feature that the calculus aims to model (e.g., plain functional, non-deterministic, probabilistic, infinitary).

The existence of different paradigms is troubling because one apparently needs to study the theory and semantics of each one separately.

We propose a unifying meta-theory of lambda-calculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambda-calculus inspired by linear logic: a bang operator marks which resources can be duplicated or discarded.

The bang calculus subsumes both call-by-name and call-by-value. A property studied in the bang calculus is automatically translated in the corresponding property for the call-by-name lambda-calculus and the call-by-value lambda-calculus, thanks to two different embeddings of the lambda-calculus in the bang calculus. These embeddings are grounded on a proof theory: they are an adaptation of Girard’s two translations of intuitionistic logic into linear logic.

Advanced computational features are usually obtained by adding new operators to a core language. Instead of studying the operational properties of the extended language from scratch, we propose a simple method to study them modularly: if an operational property holds in the core language and in the new operators separately, then a simple test of good interaction between core language and new operators guarantees that the property lifts to the whole extended language. This approach is first developed in abstract rewriting systems.