scholarly journals A Functorial Bridge Between the Infinitary Affine Lambda-Calculus and Linear Logic

2015 ◽  
pp. 144-161
Author(s):  
Damiano Mazza ◽  
Luc Pellissier
Keyword(s):  
Linear Logic ◽  
Lambda Calculus

FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness

2004 ◽  
Vol 14 (6) ◽  
pp. 623-633 ◽  
Author(s):  
HARRY G. MAIRSON
Keyword(s):  
Polynomial Time ◽  
Linear Logic ◽  
Lambda Calculus ◽  
Type Inference ◽  
Decision Problems ◽  
Logical Interpretation

We give transparent proofs of the PTIME-completeness of two decision problems for terms in the λ-calculus. The first is a reproof of the theorem that type inference for the simply-typed λ-calculus is PTIME-complete. Our proof is interesting because it uses no more than the standard combinators Church knew of some 70 years ago, in which the terms are linear affine – each bound variable occurs at most once. We then derive a modification of Church's coding of Booleans that is linear, where each bound variable occurs exactly once. A consequence of this construction is that any interpreter for linear λ-calculus requires polynomial time. The logical interpretation of this consequence is that the problem of normalizing proofnets for multiplicative linear logic (MLL) is also PTIME-complete.

Girard translation and logical predicates

2000 ◽  
Vol 10 (1) ◽  
pp. 77-89 ◽  
Author(s):  
MASAHITO HASEGAWA
Keyword(s):  
Short Proof ◽  
Linear Logic ◽  
Lambda Calculus ◽  
Independent Interest ◽  
Proof Technique ◽  
Typed Lambda Calculus ◽  
Intuitionistic Linear Logic

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.

From parametric polymorphism to models of polymorphic FPC

2009 ◽  
Vol 19 (4) ◽  
pp. 639-686 ◽  
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.

scholarly journals A lambda calculus for quantum computation with classical control

2006 ◽  
Vol 16 (3) ◽  
pp. 527-552 ◽  
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.

Foreword

1998 ◽  
Vol 8 (6) ◽  
pp. 541-541
Author(s):  
Thomas Ehrhard ◽  
Yves Lafont ◽  
Laurent Regnier
Keyword(s):  
Computer Science ◽  
Digital Circuits ◽  
Linear Logic ◽  
Lambda Calculus ◽  
Special Issue ◽  
Mathematical Structures ◽  
Programme Committee ◽  
Process Calculi ◽  
Proof Search ◽  
Abstract Machines

This special issue is devoted to complete and revised versions of papers presented at the Logique et Modèles du Calcul (Logic and Models of Computation) Conference held at CIRM in Marseilles in September 1996.The conference was organized by Marie-Renée Donnadieu, and the members of the programme committee were Gérard Berry, Jean-Yves Girard, Max Kanovich, Jean-Louis Krivine, Yves Lafont and François Lamarche.The scope of the conference was quite large, including, for instance, digital circuits, process calculi, abstract machines for lambda-calculus, computational interpretations of linear logic and logical aspects of proof search. Only the last three topics are represented in this special issue of Mathematical Structures in Computer Science, but we think that these papers are quite representative of the liveliness of research in this area on the borderline between mathematics and computing.We wish to thank Giuseppe Longo, who kindly proposed publishing this issue. For editorial reasons, a few contributions could not be included – they should appear in later issues.

Lambda Calculus with Types

2009 ◽  
Author(s):  
Henk Barendregt ◽  
Wil Dekkers ◽  
Richard Statman
Keyword(s):  
Lambda Calculus

A lambda calculus with naive substitution

1979 ◽  
Vol 28 (3) ◽  
pp. 269-282 ◽  
Author(s):  
John Staples
Keyword(s):  
Lambda Calculus ◽  
Classical Case ◽  
Syntactic Theory ◽  
Alternative Approach ◽  
New Formulation

AbstractAn alternative approach is proposed to the basic definitions of the lassical lambda calculus. A proof is sketched of the equivalence of the approach with the classical case. The new formulation simplifies some aspects of the syntactic theory of the lambda calculus. In particular it provides a justification for omitting in syntactic theory discussion of changes of bound variable.

Sign in / Sign up

Export Citation Format

Share Document