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