ABSTRACT. The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite non-determinism and indeed these languages are essentially non-deterministic. Based on a recently introduced categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces, this talk will present a deterministic version of the differential lambda-calculus. One nice feature of this new approach to differentiation is that it is compatible with general fixpoints of terms, so our language is actually a differential extension of PCF.

ABSTRACT. This paper is devoted to design computational systems of linear logic (i.e. systems in which, notably, the non linear and structural phenomena which arise during the cut-elimination process are taken in charge by specific modalities, the exponentials: ! and ?). The systems designed are “intermediate” between Intuitionistic LL and Classical LL. Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in Classical LL – and this without to loose the computational properties (closure by cut-elimination, atomizability of axioms). Three main systems are designed (Dissymetrical LL, semi-functorial Dissymetrical LL, semi-specialized Dissymetrical LL), where, in each of them, ! and ? play well differentiated roles.

ABSTRACT. Bellin translates multiplicative-additive linear logic to its intuitionistic fragment via the Chu construction, seemingly posing an alternative to negative translation. However, his translation is not sound in the sense that not all valid intuitionistic sequents in its image correspond to valid classical ones. By directly analyzing two-sided classical sequents, we develop a sound generalization thereof inspired by parametric negative translation that also handles the exponentials.

ABSTRACT. We propose to examine some of the proof theory of arithmetic by using two proof systems. A linearized version of arithmetic is available using muMALL, which is MALL plus the following logical connective to treat first-order term structures: equality and inequality, first-order universal and existential quantification, and the least and greatest fixed point operators. The proof system muLK is an extension of muMALL in which contraction and weakening are permitted. It is known that muMALL has a cut-elimination result and is therefore consistent. We will show that muLK is consistent by embedding it into second-order linear logic. We also show that muLK contains Peano arithmetic and that in a couple of different situations, muLK is conservative over muMALL. Finally, we show that a proof that a relation represents a total function can be turned into a proof-search-based algorithm to compute that function.

ABSTRACT. Plotkin's call-by-value (CbV, for short) lambda-calculus is a variant of the lambda-calculus that models the evaluation mechanism in most functional programming languages. The theory of the CbV lambda-calculus is not as well studied as the call-by-name one, because of some technical issues due to the "weakness" of Plotkin's CbV beta-rule, which leads to a mismatch between syntax and semantics. By adopting a Curry-Howard perspective, we show how linear logic inspires several ways to solve the mismatch between syntax and semantics in CbV, paving the way for restoring a theory of the CbV lambda-calculus as elegant as the one for call-by-name. We test our approach on a type-theoretic/semantic characterization of normalizabilty and on the notion of solvability.

ABSTRACT. This paper displays a linear sequent calculus in accordance with the no-cloning and no-deleting theorems of quantum computing. The calculus represents operations on matrices in terms of linear sequent rules, satisfing admissibility of cut. It is possible to define a non-trivial categorical semantics for it using categories intrinsic to vector spaces extended with a Kronecker product, which can be viewed as a partial answer to a problem posed by Abramsky.