Typed Lambda Calculi And Applications: 8th International Conference, Tlca 2007, Paris, France, June 26-28, 2007, Proceedings (lecture Notes In Computer Science)

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. 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 $\bar\lambda\mu$ -Calculus....Pages 381-395 Back Matter....Pages -