Typed Lambda Calculi and Applications

Typed Lambda Calculi and Applications: 4th International Conference, TLCA’99 L’Aquila, Italy, April 7–9, 1999 Proceedings<br />Author: Jean-Yves Girard<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-65763-7<br /> DOI: 10.1007/3-540-48959-2<br /><br />Table of Contents:<p></p><ul><li>The Coordination Language Facility and Applications </li><li>AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem </li><li>Modules in Non-commutative Logic </li><li>Elementary Complexity and Geometry of Interaction </li><li>Quantitative Semantics Revisited </li><li>Total Functionals and Well-Founded Strategies </li><li>Counting a Type’s Principal Inhabitants </li><li>Useless-Code Detection and Elimination for PCF with Algebraic Data Types </li><li>Every Unsolvable λ Term has a Decoration </li><li>Game Semantics for Untyped λβη-Calculus </li><li>A Finite Axiomatization of Inductive-Recursive Definitions </li><li>Lambda Definability with Sums via Grothendieck Logical Relations </li><li>Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value </li><li>Soundness of the Logical Framework for Its Typed Operational Semantic </li><li>Logical Predicates for Intuitionistic Linear Type Theories </li><li>Polarized Proof-Nets: Proof-Nets for LC </li><li>Call-by-Push-Value: A Subsuming Paradigm </li><li>A Study of Abramsky’s Linear Chemical Abstract Machine </li><li>Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version) </li><li>A Curry-Howard Isomorphism for Compilation and Program Execution</li></ul>