Title: Typed Lambda Calculi and Applications
Description: 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>
Subjects: Lambda calculus, Congresses