Lambda Calculus, Linear Logic and Symbolic Computation

Dossier scientifique pour l'obtention de l'habilitation à diriger les recherches

Manzonetto Giulio

Defended on March 7^th, 2017.

Reviewers: Jean Goubault-Larrecq (ENS-Cachan), Martin Hyland (Univesity of Cambridge), Jan Willem Klop (Vrije Universiteit).

Jury members: Henk Barendregt (Radboud University), Christophe Fouqueré (Université Paris-Nord), Mai Gehrke (Université Paris-Diderot), Jean Goubault-Larrecq (ENS-Cachan), Stefano Guerrini (Université Paris-Nord), Martin Hyland (University of Cambridge), Delia Kesner (Université Paris-Diderot).

Lambda Calculus, Linear Logic and Symbolic Computation, mémoire d'habilitation, 2017. [.pdf].
Slides, March 7^th, 2017. [.pdf].

This manuscript presents recent advances in the theory of functional programming languages and in the algebraization of multi-valued logics.
A recurrent theme concerns the problem of characterizing the observational equivalences between programs by means of denotational semantics arising from linear logic.

Chapter 1 illustrates new results concerning old problems in the area of λ-calculus. On the one side we provide necessary and sufficient conditions for relational models to be fully abstract for Morris's original theory, and we show that such a theory satisfy a strong extensionality condition called "the ω-rule". On the other side we show a perhaps unexpected connection between the definability problem in simply typed λ-calculus and the inhabitation problem of intersection types. Finally, we provide a normalization result for the second-order programming language ML^F.

Chapter 2 focuses on a resource sensitive extension of λ-calculus known as the resource calculus and born from Ehrhard's differential λ-calculus. On the syntactic side, we show that the equivalent of Bohm's theorem holds namely that all Taylor-eta-distinct normal forms can be separated. On the semantic side, we provide a notion of linear reflexive object living in a Cartesian closed differential category as a sound model of such a calculus. We show that this notion is general enough to encompass all known examples, including the relational semantics of linear logic.

Chapter 3 is devoted to construct denotational models of non-deterministic programming languages. First, we construct relational models of Call-By-Name and Call-By-Value λ-calculi extended with non-deterministic choice and parallel composition. Second, we provide a categorical construction based on biproduct completions and idempotent splitting for building quantitative models of non deterministic extensions of PCF. This includes a weighted relational semantics that allow to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF).

Chapter 4 provides an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.

Other resources:

a recent CV [.pdf];
all my publications are available here.

Last update: 07/03/2017