Girard translation and logical predicates

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.

Download Full-text

Syntactic soundness proof of a type-and-capability system with hidden state

Journal of Functional Programming ◽

10.1017/s0956796812000366 ◽

2012 ◽

Vol 23 (1) ◽

pp. 38-144 ◽

Cited By ~ 12

Author(s):

FRANÇOIS POTTIER

Keyword(s):

Linear Logic ◽

Scale Up ◽

Type System ◽

The Other ◽

Formal Definition ◽

Proof Technique ◽

The Core ◽

Proof Techniques ◽

Definition Of ◽

Intuitionistic Linear Logic

AbstractThis paper presents a formal definition and machine-checked soundness proof for a very expressive type-and-capability system, that is, a low-level type system that keeps precise track of ownership and side effects. The programming language has first-class functions and references. The type system's features include the following: universal, existential, and recursive types; subtyping; a distinction between affine and unrestricted data; support for strong updates; support for naming values and heap fragments via singleton and group regions; a distinction between ordinary values (which exist at runtime) and capabilities (which do not); support for dynamic reorganizations of the ownership hierarchy by disassembling and reassembling capabilities; and support for temporarily or permanently hiding a capability via frame and anti-frame rules. One contribution of the paper is the definition of the type-and-capability system itself. We present the system as modularly as possible. In particular, at the core of the system, the treatment of affinity, in the style of dual intuitionistic linear logic, is formulated in terms of an arbitrarymonotonic separation algebra, a novel axiomatization of resources, ownership, and the manner in which they evolve with time. Only the peripheral layers of the system are aware that we are dealing with a specific monotonic separation algebra, whose resources are references and regions. This semi-abstract organization should facilitate further extensions of the system with new forms of resources. The other main contribution is a machine-checked proof of type soundness. The proof is carried out in the Wright and Felleisen's syntactic style. This offers an evidence that this relatively simple-minded proof technique can scale up to systems of this complexity, and constitutes a viable alternative to more sophisticated semantic proof techniques. We do not claim that the syntactic technique is superior: We simply illustrate how it is used and highlight its strengths and shortcomings.

Download Full-text

Cut-Elimination for Full Intuitionistic Linear Logic

BRICS Report Series ◽

10.7146/brics.v3i10.19973 ◽

1996 ◽

Vol 3 (10) ◽

Cited By ~ 4

Author(s):

Torben Braüner ◽

Valeria De Paiva

Keyword(s):

Linear Logic ◽

Formal System ◽

Independent Interest ◽

Full Detail ◽

Cut Elimination ◽

Full Proof ◽

Intuitionistic Linear Logic

We describe in full detail a solution to the problem of proving the cut elimination theorem for FILL, a variant of (multiplicative and exponential-free) Linear Logic introduced by Hyland and de Paiva. Hyland and de Paiva's work used a term assignment system to describe FILL and barely sketched the proof of cut elimination. In this paper, as well as correcting a small mistake in their paper and extending the system to deal with exponentials, we introduce a different formal system describing the intuitionistic character of FILL and we provide a full proof of the cut elimination theorem. The formal system is based on a notion of dependence between formulae within a given proof and seems of independent interest. The procedure for cut elimination applies to (classical) multiplicative Linear Logic, and we can (with care) restrict our attention to the subsystem FILL. The proof, as usual with cut elimination proofs, is a little involved and we have not seen it published anywhere.

Download Full-text

From parametric polymorphism to models of polymorphic FPC

Mathematical Structures in Computer Science ◽

10.1017/s096012950900766x ◽

2009 ◽

Vol 19 (4) ◽

pp. 639-686 ◽

Cited By ~ 2

Author(s):

RASMUS EJLERS MØGELBERG

Keyword(s):

Fixed Point ◽

Intuitionistic Logic ◽

Classical Result ◽

Linear Logic ◽

Lambda Calculus ◽

Parametric Models ◽

Domain Theory ◽

Adequate Model ◽

Typed Lambda Calculus ◽

Parametric Polymorphism

This paper shows how PILLY(Polymorphic Intuitionistic/Linear Lambda calculus with a fixed point combinatorY) with parametric polymorphism can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using Plotkin's encodings of recursive types in PILLY, we show how parametric models of PILLYgive rise to models of FPC, which is a simply typed lambda calculus with recursive types and an operational call-by-value semantics, reflecting a classical result from domain theory. Essentially, this interpretation is an interpretation of intuitionistic logic into linear logic first discovered by Girard, which in this paper is extended to deal with recursive types. Of particular interest is a model based on ‘admissible’ pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is to the author's knowledge the first denotational model of a non-linear language with parametric polymorphism and recursive types.

Download Full-text

A lambda calculus for quantum computation with classical control

Mathematical Structures in Computer Science ◽

10.1017/s0960129506005238 ◽

2006 ◽

Vol 16 (3) ◽

pp. 527-552 ◽

Cited By ~ 68

Author(s):

PETER SELINGER ◽

BENOIT VALIRON

Keyword(s):

Linear Logic ◽

Operational Semantics ◽

Type System ◽

Lambda Calculus ◽

Quantum Computers ◽

Safety Properties ◽

Control Paradigm ◽

Flow Charts ◽

Classical Control ◽

Intuitionistic Linear Logic

In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ‘quantum data, classical control’ paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

Download Full-text