Typed Lambda Calculi and Applications

About this book

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