Typed Lambda Calculi and Applications: 8th International Conference,TLCA 2007, Paris, France,June 26-28, 2007. Proceedings

Frank Pfenning (auth.), Simona Ronchi Della Rocca (eds.)3540732276, 9783540732273, 9783540732280

This book constitutes the refereed proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007, held in Paris, France in June 2007 in conjunction with RTA 2007, the 18th International Conference on Rewriting Techniques and Applications as part of RDP 2007, the 4th International Conference on Rewriting, Deduction, and Programming.

The 25 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 52 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.

---

Table of contents :
Front Matter….Pages –
On a Logical Foundation for Explicit Substitutions….Pages 1-1
From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing….Pages 2-7
Strong Normalization and Equi-(Co)Inductive Types….Pages 8-22
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves….Pages 23-38
The Safe Lambda Calculus….Pages 39-53
Intuitionistic Refinement Calculus….Pages 54-69
Computation by Prophecy….Pages 70-83
An Arithmetical Proof of the Strong Normalization for the λ -Calculus with Recursive Equations on Types….Pages 84-101
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo….Pages 102-117
Completing Herbelin’s Programme….Pages 118-132
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi….Pages 133-147
Ludics is a Model for the Finitary Linear Pi-Calculus….Pages 148-162
Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic….Pages 163-177
The Omega Rule is $mathbf{Pi_{1}^{1}}$ -Complete in the λβ -Calculus….Pages 178-193
Weakly Distributive Domains….Pages 194-206
Initial Algebra Semantics Is Enough!….Pages 207-222
A Substructural Type System for Delimited Continuations….Pages 223-239
The Inhabitation Problem for Rank Two Intersection Types….Pages 240-254
Extensional Rewriting with Sums….Pages 255-271
Higher-Order Logic Programming Languages with Constraints: A Semantics….Pages 272-289
Predicative Analysis of Feasibility and Diagonalization….Pages 290-304
Edifices and Full Abstraction for the Symmetric Interaction Combinators….Pages 305-320
Two Session Typing Systems for Higher-Order Mobile Processes….Pages 321-335
An Isomorphism Between Cut-Elimination Procedure and Proof Reduction….Pages 336-350
Polynomial Size Analysis of First-Order Functions….Pages 351-365
Simple Saturated Sets for Disjunction and Second-Order Existential Quantification….Pages 366-380
Convolution $barlambdamu$ -Calculus….Pages 381-395
Back Matter….Pages –