Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

The subtyping relation of programming languages can be analysed as an entailment relation by means of proof theory. We are interested in two main families of systems: intersection types and polymorphic subtyping. They share the fact that implication has some distributivity property: over intersection in the first case and over universal quantification in the second one. We introduce a restriction of the second-order (full) Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. This new system IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping relations. We recover sequent calculi from the literature (as well as new variants) as restrictions of IS (thanks to the proof-theoretical analysis of the system: admissible rules, invertibility, focusing, etc.), so that IS appears as a unifying logic for subtyping. We also develop translations relating IS with relevant logic, the (unconstrained) Lambek calculus or cyclic linear logic.

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

International audience

We investigate the possibility of formalizing quantifiers in proof theory while avoiding, as far as possible, the use of true binding structures, α-equivalence or variable renamings. We propose a solution with two kinds of variables in terms and formulas, as originally done by Gentzen. In this way formulas are first-order structures, and we are able to avoid capture problems in substitutions. However at the level of proofs and proof manipulations, some binding structure seems unavoidable. We give a representation with de Bruijn indices for proof rules which does not impact the formula representation and keeps the whole set of definitions first-order.

Abstract We present a framework for game semantics based on concurrent games, that keeps track of resources as data modified throughout execution but not affecting its control flow. Our leading example is time, yet the construction is in fact parametrized by a resource bimonoid $$\mathcal {R}$$ , an algebraic structure expressing resources and the effect of their consumption either sequentially or in parallel. Relying on our construction, we give a sound resource-sensitive denotation to $$\mathcal {R}$$ -IPA, an affine higher-order concurrent programming language with shared state and a primitive for resource consumption in $$\mathcal {R}$$ . Compared with general operational semantics parametrized by $$\mathcal {R}$$ , our resource analysis turns out to be finer, leading to non-adequacy. Yet, our model is not degenerate as adequacy holds for an operational semantics specialized to time. In regard to earlier semantic frameworks for tracking resources, the main novelty of our work is that it is based on a non-interleaving semantics, and as such accounts for parallel use of resources accurately.

We revisit many aspects of the syntactic relations between (variants of) classical linear logic (LL) and (variants of) intuitionistic linear logic (ILL) in the propositional setting.

We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a “cut-elimination” property.

The intuitionistic sequent calculus (at most one formula on the right-hand side of sequents) comes with a natural dual system: the dual-intuitionistic sequent calculus (at most one formula on the left-hand side). We explain how the duality between these two systems exactly corresponds to the intensively studied duality between call-by-value systems and call-by-name systems for classical logic. Relying on the uniqueness of the computational behaviour underlying these four logics (intuitionistic, dual-intuitionistic, call-by-value classical and call-by-name classical), we define a generic syntax of nets which can be used for any of these logics.

We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard's one. It is also based on the use of monomial weights for identifying additive components (slices). Our generalization gives the possibility of representing a kind of sharing of nodes which does not exist in Girard's nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be stable by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.

We give a semantic characterization of bounded complexity proofs. We introduce the notion of obsessional clique in the relational model of linear logic and show that restricting the morphisms of the category REL to obsessional cliques yields models of ELL and SLL. Conversely, we prove that these models are relatively complete: an LL proof whose interpretation is an obsessional clique is always an ELL/SLL proof. These results are achieved by introducing a system of ELL/SLL untyped proof-nets, which is both correct and complete with respect to elementary/ polynomial time

The study of isomorphisms of types has, in the main, been carried out in an intuitionistic setting. We extend some of this work to classical logic for both call-by-name and call-by-value computations by means of polarised linear logic and game semantics. This leads to equational characterisations of these isomorphisms for all the propositional connectives.

We show that the decomposition of intuitionistic logic into linear logic along the equation A /spl rarr/ B = !A /spl rarr/ B may be adapted into a decomposition of classical logic into LLP, the polarized version of Linear Logic. Firstly, we build a categorical model of classical logic (a control category) from a categorical model of linear logic by a construction similar to the co-Kleisli category. Secondly, we analyze two standard continuation-passing style (CPS) translations, the Plotkin and the Krivine's translations, which are shown to correspond to two embeddings of LLP into LL.

We generalize the intuitionistic Hyland-Ong games to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding a game model for polarized linear logic with a definability result. As a consequence this gives a complete game model for various classical systems: LC, /spl lambda//spl mu/-calculus,... for both call-by-name and call-by-value evaluations.