Research Catalog

Title

Typed lambda calculi and applications : 4th international conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999 : proceedings / Jean-Yves Girard (ed.)

Author

International Conference on Typed Lambda Calculi and Applications (4th : 1999 : L'Aquila, Italy)

Publication

New York : Springer, 1999.

Items in the Library & Off-site

Holdings

Details

Additional Authors

Girard, Jean-Yves.

Description

viii, 396 pages; 24 cm.

Series Statement

Lecture notes in computer science ; 1581

Uniform Title

Lecture notes in computer science ; 1581.

Subject

• Lambda calculus > Congresses

Bibliography (note)

• Includes bibliographical references and index.

Contents

The Coordination Language Facility and Applications / J.-M. Andreoli -- AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem / P. H. Eidorff, F. Henglein and C. Mossin -- Modules in Non-commutative Logic / V. M. Abrusci -- Elementary Complexity and Geometry of Interaction / P. Baillot and M. Pedicini -- Quantitative Semantics Revisited / N. Barreiro and T. Ehrhard -- Total Functionals and Well-Founded Strategies / S. Berardi and U. de'Liguoro -- Counting a Type's Principal Inhabitants / S. Broda and L. Damas -- Useless-Code Detection and Elimination for PCF with Algebraic Data types / F. Damiani -- Every Unsolvable [lambda] Term has a Decoration / R. David -- Game Semantics for Untyped [lambda][beta][eta]-Calculus / P. Di Gianantonio, G. Franco and F. Honsell -- A Finite Axiomatization of Inductive-Recursive Definitions / P. Dybjer and A. Setzer -- Lambda Definability with Sums via Grothendieck Logical Relations / M. Fiore and A. Simpson -- Explicitly Typed [lambda][mu]-Calculus for Polymorphism and Call-by-Value / K. Fujita -- Soundness of the Logical Framework for Its Typed Operational Semantics / H. Goguen -- Logical Predicates for Intuitionistic Linear Type Theories / M. Hasegawa -- Polarized Proof-Nets: Proof-Nets for LC / O. Laurent -- Call-by-Push-Value: A Subsuming Paradigm / P. B. Levy -- A Study of Abramsky's Linear Chemical Abstract Machine / S. Mikami and Y. Akama -- Resource Interpretations, Bunched Implications and the [alpha][lambda]-Calculus / P. W. O'Hearn -- A Curry-Howard Isomorphism for Compilation and Program Execution / A. Ohori -- Natural Deduction for Intuitionistic Non-commutative Linear Logic / J. Polakow and F. Pfenning -- A Logic for Abstract Data Types as Existential Types / E. Poll and J. Zwanenburg -- Characterising Explicit Substitutions which Preserve Termination / E. Ritter -- Explicit Environments / M. Sato, T. Sakurai and R. Burstall -- Consequences of Jacopini's Theorem: Consistent Equalities and Equations / R. Statman -- Strong Normalisation of Cut-Elimination in Classical Logic / C. Urban and G. M. Bierman -- Pure Type Systems with Subtyping / J. Zwanenburg.

ISBN

3540657630 (alk. paper)

LCCN

99014931

OCLC

• 504320201
• ocn504320201

Owning Institutions

Columbia University Libraries