Invited workshop talk: Giulio Guerrieri
Our new team member Giulio is giving an invited talk at LSFA, an FSCD-associated workshop. More details on the workshop web page:
Understanding the lambda-calculus via (non-)linearity and rewriting.
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 features 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 and uniform 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 Girard’s linear logic and Levy’s Call-by-Push-Value: 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 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.