Typed Lambda Calculi and Applications: 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (Lecture Notes in Computer Science, 1581)

This book constitutes the refereed proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, TLCA'99, held in L'Aquila, Italy in April 1999. The 25 revised full papers presented were carefully reviewed and selected from a total of 50 submissions. Also included are two invited demonstrations. The volume reports research results on various aspects of typed lambda calculi. Among the topics addressed are noncommutative logics, type theory, algebraic data types, logical calculi, abstract data types, and subtyping. The Coordination Language Facility and Applications....Pages 1-5 AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem....Pages 6-13 Modules in Non-commutative Logic....Pages 14-24 Elementary Complexity and Geometry of Interaction....Pages 25-33 Quantitative Semantics Revisited....Pages 40-53 Total Functionals and Well-Founded Strategies....Pages 54-68 Counting a Type’s Principal Inhabitants....Pages 69-82 Useless-Code Detection and Elimination for PCF with Algebraic Data Types....Pages 83-97 Every Unsolvable λ Term has a Decoration....Pages 98-113 Game Semantics for Untyped λβη -Calculus....Pages 114-128 A Finite Axiomatization of Inductive-Recursive Definitions....Pages 129-146 Lambda Definability with Sums via Grothendieck Logical Relations....Pages 147-161 Explicitly Typed λ μ -Calculus for Polymorphism and Call-by-Value....Pages 162-177 Soundness of the Logical Framework for Its Typed Operational Semantic....Pages 177-197 Logical Predicates for Intuitionistic Linear Type Theories....Pages 198-213 Polarized Proof-Nets: Proof-Nets for LC....Pages 213-227 Call-by-Push-Value: A Subsuming Paradigm....Pages 228-243 A Study of Abramsky’s Linear Chemical Abstract Machine....Pages 243-257 Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version)....Pages 258-279 A Curry-Howard Isomorphism for Compilation and Program Execution....Pages 280-294 Natural Deduction for Intuitionistic Non-commutative Linear Logic....Pages 295-309 A Logic for Abstract Data Types as Existential Types....Pages 310-324 Characterising Explicit Substitutions which Preserve Termination....Pages 325-339 Explicit Environments....Pages 340-354 Consequences of Jacopini’s Theorem: Consistent Equalities and Equations....Pages 355-364 Strong Normalisation of Cut-Elimination in Classical Logic....Pages 365-380 Pure Type Systems with Subtyping....Pages 381-396 Typed Lambda Calculi and Applications: 4th International Conference, TLCA’99 L’Aquila, Italy, April 7–9, 1999 Proceedings Author: Jean-Yves Girard Published by Springer Berlin Heidelberg ISBN: 978-3-540-65763-7 DOI: 10.1007/3-540-48959-2 Table of Contents: The Coordination Language Facility and Applications AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem Modules in Non-commutative Logic Elementary Complexity and Geometry of Interaction Quantitative Semantics Revisited Total Functionals and Well-Founded Strategies Counting a Type’s Principal Inhabitants Useless-Code Detection and Elimination for PCF with Algebraic Data Types Every Unsolvable λ Term has a Decoration Game Semantics for Untyped λβη-Calculus A Finite Axiomatization of Inductive-Recursive Definitions Lambda Definability with Sums via Grothendieck Logical Relations Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value Soundness of the Logical Framework for Its Typed Operational Semantic Logical Predicates for Intuitionistic Linear Type Theories Polarized Proof-Nets: Proof-Nets for LC Call-by-Push-Value: A Subsuming Paradigm A Study of Abramsky’s Linear Chemical Abstract Machine Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version) A Curry-Howard Isomorphism for Compilation and Program Execution