Skip to main content

2009 | Buch

Typed Lambda Calculi and Applications

9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings

insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th International Conference on Rewriting Techniques and Applications as part of RDP 2009, the 5th International Conference on Rewriting, Deduction, and Programming. The 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. The papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.

Inhaltsverzeichnis

Frontmatter
Mathematical Synthesis of Equational Deduction Systems
Abstract
Our view of computation is still evolving. The concrete theories for specific computational phenomena that are emerging encompass three aspects: specification and programming languages for describing computations, mathematical structures for modelling computations, and logics for reasoning about properties of computations. To make sense of this complexity, and also to compare and/or relate different concrete theories, meta-theories have been built. These metatheories are used for the study, formalisation, specification, prototyping, and testing of concrete theories.
Marcelo Fiore, Chung-Kil Hur
A Pronominal Approach to Binding and Computation
Abstract
There has been a great deal of research on programming languages for computing with binding and scope (bound variables, α-equivalence, capture-avoiding substitution). These languages are useful for a variety of tasks, such as implementing domain-specific languages and formalizing the metatheory of programming languages. Functional programming with binding and scope involves two different notions of function: functions-as-data and functions-as-computation. Functions-as-data, used to represent abstract syntax with variable binding, have an intensional, syntactic, character, in the sense that they can be inspected in ways other than function application. For example, many algorithms that process abstract syntax recur under binders, treating variables symbolically. On the other hand, functions-as-computation, the usual functions of functional programming, have an extensional character—a function from A to B is a black box that, when given an A, delivers a B.
Robert Harper, Daniel R. Licata, Noam Zeilberger
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
Abstract
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.
Andreas Abel, Thierry Coquand, Miguel Pagano
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
Abstract
We interpret classical proofs as constructive proofs (with constructive rules for ∨ , ∃) over a suitable structure \({\mathcal N}\) for the language of natural numbers and maps of Gödel’s system \({\mathcal{T}}\). We introduce a new Realization semantics we call “Interactive learning-based Realizability”, for Heyting Arithmetic plus EM 1 (Excluded middle axiom restricted to \(\Sigma^0_1\) formulas). Individuals of \({\mathcal N}\) evolve with time, and realizers may “interact” with them, by influencing their evolution. We build our semantics over Avigad’s fixed point result [1], but the same semantics may be defined over different constructive interpretations of classical arithmetic (in [7], continuations are used). Our notion of realizability extends Kleene’s realizability and differs from it only in the atomic case: we interpret atomic realizers as “learning agents”.
Federico Aschieri, Stefano Berardi
Syntax for Free: Representing Syntax with Binding Using Parametricity
Abstract
We show that, in a parametric model of polymorphism, the type ∀ α. ((αα) →α) →(ααα) →α is isomorphic to closed de Bruijn terms. That is, the type of closed higher-order abstract syntax terms is isomorphic to a concrete representation. To demonstrate the proof we have constructed a model of parametric polymorphism inside the Coq proof assistant. The proof of the theorem requires parametricity over Kripke relations. We also investigate some variants of this representation.
Robert Atkey
On the Meaning of Logical Completeness
Abstract
Gödel’s completeness theorem is concerned with provability, while Girard’s theorem in ludics (as well as full completeness theorems in game semantics) is concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [1], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic.
We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of \({\mathbf{A}}^{\bot}\) which beats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Gödel’s completeness, in that it explicitly constructs a countermodel essentially using König’s lemma, proceeds by induction on formulas, and implies an analogue of Löwenheim-Skolem theorem.
Michele Basaldella, Kazushige Terui
Thick Subtrees, Games and Experiments
Abstract
We relate the dynamic semantics (games, dealing with interactions) and the static semantics (dealing with results of interactions) of linear logic with polarities, in the spirit of Timeless Games [1].
The polarized game semantics is full and faithfull for polarized proof-nets [2]. We detail the correspondence between cut free proof-nets and innocent strategies, in a framework related to abstract Böhm trees.
A notion of thick subtree allows us to reveal a deep relation between plays in games and Girard’s experiments on proof-nets. We then define a desequentializing operation, forgetting time in games which coincides with the usual way of computing a result of interaction from an experiment. We then obtain our main result: desequentializing the game interpretation of a polarized proof-net yields its standard relational model interpretation (static semantics).
Pierre Boudes
Bounded Linear Logic, Revisited
Abstract
We present QBAL, an extension of Girard, Scedrov and Scott’s bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant’s RRW and Hofmann’s LFPL into QBAL.
Ugo Dal Lago, Martin Hofmann
Partial Orders, Event Structures and Linear Strategies
Abstract
We introduce a Game Semantics where strategies are partial orders, and composition is a generalization of the merging of orders. Building on this, to bridge between Game Semantics and Concurrency, we explore the relation between Event Structures and Linear Strategies. The former are a true concurrency model introduced by Nielsen, Plotkin, Winskel, the latter a family of linear innocent strategies developed starting from Girard’s work in the setting of Ludics.
We extend our construction on partial orders to classes of event structures, showing how to reduce composition of event structures to the simple definition of merging of orders. Finally, we introduce a compact closed category of event structures which embeds Linear Strategies.
Claudia Faggian, Mauro Piccolo
Existential Type Systems with No Types in Terms
Abstract
We study type checking, typability, and type inference problems for type-free style and Curry style second-order existential systems where the type-free style differs from the Curry style in that the terms of the former contain information on where the existential quantifier elimination and introduction take place but omit the information on which types are involved. We show that all the problems are undecidable employing reduction of second-order unification in case of the type-free system and semiunification in case of the Curry style system. This provides a fine border between problems yielding to a reduction of second-order unification problem and the semiunification problem. In addition, we investigate the subject reduction property of the system in the Curry-style.
Ken-etsu Fujita, Aleksy Schubert
Initial Algebra Semantics for Cyclic Sharing Structures
Abstract
Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural induction and structural recursion. In the case of graphs or ”tree-like” structures – trees involving cycles and sharing – however, it is not clear what kind of inductive structures exists and how we can faithfully assign a term representation of them. In this paper we propose a simple term syntax for cyclic sharing structures that admits structural induction and recursion principles. We show that the obtained syntax is directly usable in the functional language Haskell, as well as ordinary data structures such as lists and trees. To achieve this goal, we use categorical approach to initial algebra semantics in a presheaf category. That approach follows the line of Fiore, Plotkin and Turi’s models of abstract syntax with variable binding.
Makoto Hamana
An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
Abstract
We give a decomposition of the equational theory of call-by-value λ-calculus into a confluent rewrite system made of three independent subsystems that refines Moggi’s computational calculus:
  • the purely operational system essentially contains Plotkin’s β v rule and is necessary and sufficient for the evaluation of closed terms;
  • the structural system contains commutation rules that are necessary and sufficient for the reduction of all “computational” redexes of a term, in a sense that we define;
  • the observational system contains rules that have no proper computational content but are necessary to characterize the valid observational equations on finite normal forms.
We extend this analysis to the case of λ-calculus with control and provide with the first presentation as a confluent rewrite system of Sabry-Felleisen and Hofmann’s equational theory of λ-calculus with control.
Incidentally, we give an alternative definition of standardization in call-by-value λ-calculus that, unlike Plotkin’s original definition, prolongs weak head reduction in an unambiguous way.
Hugo Herbelin, Stéphane Zimmermann
Refinement Types as Proof Irrelevance
Abstract
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. Proof irrelevance provides a mechanism for selectively hiding the identities of terms in type theories. In this paper, we show that refinement types can be interpreted as predicates using proof irrelevance in the context of the logical framework LF, establishing a uniform relationship between two previously studied concepts in type theory. The interpretation and its correctness proof are surprisingly complex, lending credence to the idea that refinement types are a fundamental construct rather than just a convenient surface syntax for certain uses of proof irrelevance.
William Lovas, Frank Pfenning
Weak ω-Categories from Intensional Type Theory
Abstract
Higher-dimensional categories have recently emerged as a natural context for modelling intensional type theories; this raises the question of what higher-categorical structures the syntax of type theory naturally forms. We show that for any type in Martin-Löf Intensional Type Theory, the system of terms of that type and its higher identity types forms a weak ω-category in the sense of Leinster. Precisely, we construct a contractible globular operad \({P_{\mathit{ML}^{\mathrm{Id}}}}\) of type-theoretically definable composition laws, and give an action of this operad on any type and its identity types.
Peter LeFanu Lumsdaine
Relating Classical Realizability and Negative Translation for Existential Witness Extraction
Abstract
Friedman showed how to turn a classical proof of a \(\Sigma^0_1\) formula into an intuitionistic proof of the same formula, thus giving an effective method to extract witnesses from classical proofs of such formulae. In this paper we show how to achieve the same goal efficiently using Krivine realizability with primitive numerals, and prove that the corresponding program is but the direct-style equivalent (using call-cc) of the CPS-style program underlying Friedman’s method.
Alexandre Miquel
Session-Based Communication Optimisation for Higher-Order Mobile Processes
Abstract
In this paper we solve an open problem posed in our previous work on asynchronous subtyping [12], extending the method to higher-order session communication and functions. Our system provides two complementary methods for communication code optimisation, mobile code and asynchronous permutation of session actions, within processes that utilise structured, typed communications. In order to prove transitivity of our coinductive subtyping relation, we uniformly deal with type-manifested asynchrony, linear functional types, and contravariant components in higher-order communications. For the runtime system we propose a new compact formulation that takes into account stored higher-order values with open sessions, as well as asynchronous commutativity. In spite of the enriched type structures, we construct an algorithmic subtyping system, which is sound and complete with respect to the coinductive subtyping relation. The paper also demonstrates the expressiveness of our typing system with an e-commerce example, where optimised processes can interact respecting the expected sessions.
Dimitris Mostrous, Nobuko Yoshida
The Cut-Elimination Theorem for Differential Nets with Promotion
Abstract
Recently Ehrhard and Regnier have introduced Differential Linear Logic, DiLL for short — an extension of the Multiplicative Exponential fragment of Linear Logic that is able to express non-deterministic computations. The authors have examined the cut-elimination of the promotion-free fragment of DiLL by means of a proofnet-like calculus: differential interaction nets. We extend this analysis to exponential boxes and prove the Cut-Elimination Theorem for the whole DiLL: every differential net that is sequentializable can be reduced to a cut-free net.
Michele Pagani
A Polymorphic Type System for the Lambda-Calculus with Constructors
Abstract
We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. To prove the strong normalisation property for this system, we translate well-typed terms in an auxiliary calculus of case-normal forms using the interpretation method. We finally prove the strong normalisation property for the auxiliary calculus using the standard reducibility method.
Barbara Petit
Kripke Semantics for Martin-Löf’s Extensional Type Theory
Abstract
It is well-known that simple type theory is complete with respect to non-standard models. Completeness for standard models only holds when increasing the class of models, e.g., to cartesian closed categories. Similarly, dependent type theory is complete for locally cartesian closed categories. However, it is usually difficult to establish the coherence of interpretations of dependent type theory, i.e., to show that the interpretations of equal expressions are indeed equal. Several classes of models have been used to remedy this problem.
We contribute to this investigation by giving a semantics that is both coherent and sufficiently general for completeness while remaining relatively easy to compute with. Our models interpret types of Martin-Löf’s extensional dependent type theory as sets indexed over posets or, equivalently, as fibrations over posets. This semantics can be seen as a generalization to dependent type theory of the interpretation of intuitionistic first-order logic in Kripke models. This yields a simple coherent model theory with respect to which simple and dependent type theory are sound and complete.
Steve Awodey, Florian Rabe
On the Values of Reducibility Candidates
Abstract
The straightforward elimination of union types is known to break subject reduction, and for some extensions of the lambda-calculus, to break strong normalization as well. Similarly, the straightforward elimination of implicit existential types breaks subject reduction.
We propose elimination rules for union types and implicit existential quantification which use a form call-by-value issued from Girard’s reducibility candidates. We show that these rules remedy the above mentioned difficulties, for strong normalization and, for the existential quantification, for subject reduction as well.
Moreover, for extensions of the lambda-calculus based on intuitionistic logic, we show that the obtained existential quantification is equivalent to its usual impredicative encoding w.r.t. provability in realizability models built from reducibility candidates and biorthogonals.
Colin Riba
Lexicographic Path Induction
Abstract
Programming languages theory is full of problems that reduce to proving the consistency of a logic, such as the normalization of typed lambda-calculi, the decidability of equality in type theory, equivalence testing of traces in security, etc. Although the principle of transfinite induction is routinely employed by logicians in proving such theorems, it is rarely used by programming languages researchers, who often prefer alternatives such as proofs by logical relations and model theoretic constructions. In this paper we harness the well-foundedness of the lexicographic path ordering to derive an induction principle that combines the comfort of structural induction with the expressive strength of transfinite induction. Using lexicographic path induction, we give a consistency proof of Martin-Löf’s intuitionistic theory of inductive definitions. The consistency of Heyting arithmetic follows directly, and weak normalization for Gödel’s T follows indirectly; both have been formalized in a prototypical extension of Twelf.
Jeffrey Sarnat, Carsten Schürmann
Parametricity for Haskell with Imprecise Error Semantics
Abstract
Error raising, propagation, and handling in Haskell can be imprecise in the sense that a language implementation’s choice of local evaluation order, and optimizing transformations to apply, may influence which of a number of potential failure events hidden somewhere in a program is actually triggered. While this has pragmatic advantages from an implementation point of view, it also complicates the meaning of programs and thus requires extra care when reasoning about them. The proper semantic setup is one in which every erroneous value represents a whole set of potential (but not arbitrary) failure causes. The associated propagation rules are somewhat askew to standard notions of program flow and value dependence. As a consequence, standard reasoning techniques are cast into doubt, and rightly so. We study this issue in depth for one such reasoning technique, namely the derivation of free theorems from polymorphic types. We revise and extend the foundational notion of relational parametricity, as well as further material required to make it applicable.
Florian Stenger, Janis Voigtländer
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
Abstract
We investigate the question of what constitutes a proof when quantifiers and multiplicative units are both present. On the technical level this paper provides two new aspects of the proof theory of MLL2 with units. First, we give a novel proof system in the framework of the calculus of structures. The main feature of the new system is the consequent use of deep inference, which allows us to observe a decomposition which is a version of Herbrand’s theorem that is not visible in the sequent calculus. Second, we show a new notion of proof nets which is independent from any deductive system. We have “sequentialisation” into the calculus of structures as well as into the sequent calculus. Since cut elimination is terminating and confluent, we have a category of MLL2 proof nets. The treatment of the units is such that this category is star-autonomous.
Lutz Straßburger
Algebraic Totality, towards Completeness
Abstract
Finiteness spaces constitute a categorical model of Linear Logic (LL) whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we recall definitions of finiteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give an interpretation of LL based on linear algebra. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed affine subspace which does not contain 0. We show that finiteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans \({\mathcal{B}}\) and a conditional operator, which can be interpreted in this model. We prove completeness at type \({\mathcal{B}}^n\to{\mathcal{B}}\) for every n by an algebraic method.
Christine Tasson
A Logical Foundation for Environment Classifiers
Abstract
Taha and Nielsen have developed a multi-stage calculus λ α with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable.
In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by developing a typed λ-calculus λ  ⊳ . It corresponds to multi-modal logic that allows quantification by transition variables—a counterpart of classifiers—which range over (possibly empty) sequences of labeled transitions between possible worlds. This interpretation will reduce the “run” construct—which has a special typing rule in λ α —and embedding of closed code into other code fragments of different stages—which would be only realized by the cross-stage persistence operator in λ α —to merely a special case of classifier application. We prove that λ  ⊳  enjoys basic properties including subject reduction, confluence, and strong normalization and that the execution of a well-typed λ  ⊳  program is properly staged. Finally, we show that the proof system augmented with a classical axiom is sound and complete with respect to a Kripke semantics of the logic.
Takeshi Tsukada, Atsushi Igarashi
Inhabitation of Low-Rank Intersection Types
Abstract
We prove that the inhabitation problem (“Does there exist a closed term of a given type?”) is undecidable for intersection types of rank 3 and exponential space complete for intersection types of rank 2.
Paweł Urzyczyn
Differential Linear Logic and Polarization
Abstract
We extend Ehrhard–Regnier’s differential linear logic along the lines of Laurent’s polarization. We provide a denotational semantics of this new system in the well-known relational model of linear logic, extending canonically the semantics of both differential and polarized linear logics: this justifies our choice of cut elimination rules. Then we show this polarized differential linear logic refines the recently introduced convolution \({\bar\lambda}\mu\)-calculus, the same as linear logic decomposes λ-calculus.
Lionel Vaux
Complexity of Gödel’s T in λ-Formulation
Abstract
Let T be Gödel’s system of primitive recursive functionals of finite type in the λ-formulation. We define by constructive means using recursion on nested multisets a multivalued function I from the set of terms of T into the set of natural numbers such that if a term a reduces to a term b and if a natural number I(a) is assigned to a then a natural number I(b) can be assigned to b such that I(a) > I(b). The construction of I is based on Howard’s 1970 ordinal assignment for T and Weiermann’s 1996 treatment of T in the combinatory logic version. As a corollary we obtain an optimal derivation length classification for the λ-formulation of T and its fragments. Compared with Weiermann’s 1996 exposition this article yields solutions to several non-trivial problems arising from dealing with λ-terms instead of combinatory logic terms.
Gunnar Wilken, Andreas Weiermann
The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
Abstract
Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann’s SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. We in particular define rules that justify directly the computational indistinguishability between programs and prove that these rules are sound with respect to the set-theoretic semantics, hence the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali’s construction of pseudorandom generator.
Yu Zhang
Backmatter
Metadaten
Titel
Typed Lambda Calculi and Applications
herausgegeben von
Pierre-Louis Curien
Copyright-Jahr
2009
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-02273-9
Print ISBN
978-3-642-02272-2
DOI
https://doi.org/10.1007/978-3-642-02273-9