Typed Lambda Calculi and Applications
Subtitle: 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (Lecture Notes in Computer Science)
Edition: 1 edition
Publisher: Springer
Published: April 28, 1999
Language: eng
Format: Paperback
Number of pages: 397
ISBN-13: 9783540657637
Subjects: Calculus & mathematical analysis; Mathematical logic; Mathematical theory of computation; Systems analysis & design; Philosophy Of Mathematics; Mathematical And Symbolic Logic; Mathematics; Science/Mathematics; General; Logic; Mathematics / Logic; Lambda calculus; Congresses
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>