Catálogo de publicaciones - libros

The so-called light logics [1,2,3] have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic, as discussed in [4]. In this paper we show that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic (EAL), designing a type system in natural deduction style assigning EAL formulae to lambda terms.

Let ⊢ be a rank-2 intersection type system. We say that a term is ⊢ -simple (or just simple when the system ⊢ is clear from the context) if system ⊢ can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type recursive definitions that are not simple. At the best of our knowledge, previous algorithms for typing recursive definitions in the presence of rank-2 intersection types allow only simple recursive definitions to be typed. The proposed rules are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec { x = e } where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank-2 intersection, so they can be applied to other type systems.

The symmetric λμ -calculus is the λμ -calculus introduced by Parigot in which the reduction rule μ ′, which is the symmetric of μ , is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the μμ ′-reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the βμ μ ′-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.

This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class interfaces. The tool returns classes in the library that can be used to implement the user’s request and automatically builds the required glue code. We propose subtyping of recursive types in the presence of associative and commutative products—that is, subtyping modulo a restricted form of type isomorphisms—as a model of the relation that exists between the user’s query and the tool’s answers. We show that this relation is a composition of the standard subtyping relation with equality up to associativity and commutativity of products and we present an efficient decision algorithm for it. We also provide an automatic way of constructing coercions between related types.

We show that there exist bijective translations between polymorphic λ -calculus and a subsystem of minimal logic with existential types, which form a Galois connection and moreover a Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.

We show that a minimal dependent type theory based on Σ-types and equality is degenerated in presence of computational classical logic. By computational classical logic is meant a classical logic derived from a control operator equipped with reduction rules similar to the ones of Felleisen’s ${\mathcal C}$ or Parigot’s μ operators. As a consequence, formalisms such as Martin-Löf’s type theory or the ( Set -predicative variant of the) Calculus of Inductive Constructions are inconsistent in presence of computational classical logic. Besides, an analysis of the role of the η -rule for control operators through a set-theoretic model of computational classical logic is given.

Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, that relies on completeness of the cut-free calculus with respect to Kripke Models. The proof defines a general framework to extend the cut elimination result to other intuitionistic deduction systems, in particular to deduction modulo provided the rewrite system verifies some properties. We also give an example of rewrite system for which cut elimination holds but that doesn’t enjoys proof normalization.

We use a fully abstract denotational model to show that nested function calls and recursive definitions can be eliminated from SPCF (a typed functional language with simple non-local control operators) without losing expressiveness. We describe — via simple typing rules — an affine fragment of SPCF in which function nesting and recursion (other than iteration) are not permitted. We prove that this affine fragment is fully expressive in the sense that every term of SPCF is observationally equivalent to an affine term. Our proof is based on the observation of Longley — already used to prove universality and full abstraction results for models of SPCF — that every type of SPCF is a retract of a first-order type. We describe retractions of this kind which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) normal form, and then projecting back to the original type. In the case of finitary SPCF, the retraction is based on a simple induction, which yields bounds for the size of the resulting term. In the infinitary case, it is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.

We present a theory of proof denotations in classical propositional logic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a “Boolean” category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a “real” sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.

We propose ⊤ ⊤- lifting as a technique for extending operational predicates to Moggi’s monadic computation types, independent of the choice of monad. We demonstrate the method with an application to Girard-Tait reducibility, using this to prove strong normalisation for the computational metalanguage  λ _ ml . The particular challenge with reducibility is to apply this semantic notion at computation types when the exact meaning of “computation” (stateful, side-effecting, nondeterministic, etc.) is left unspecified. Our solution is to define reducibility for continuations and use that to support the jump from value types to computation types. The method appears robust: we apply it to show strong normalisation for the computational metalanguage extended with sums, and with exceptions. Based on these results, as well as previous work with local state, we suggest that this “leap-frog” approach offers a general method for raising concepts defined at value types up to observable properties of computations.