2. TLCA 1995: Edinburgh, UK

Mariangiola Dezani-Ciancaglini, Gordon D. Plotkin (Eds.): Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings. Lecture Notes in Computer Science 902 Springer 1995, ISBN 3-540-59048-X

@proceedings{DBLP:conf/tlca/1995,
  editor    = {Mariangiola Dezani-Ciancaglini and
               Gordon D. Plotkin},
  title     = {Typed Lambda Calculi and Applications, Second International Conference
               on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh,
               UK, April 10-12, 1995, Proceedings},
  booktitle = {TLCA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {902},
  year      = {1995},
  isbn      = {3-540-59048-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Andrea Asperti, Cosimo Laneve: Comparing Lambda-calculus translations in Sharing Graphs. 1-15
Gilles Barthe: Extensions of Pure Type Systems. 16-31
Roberto Bellucci, Martín Abadi, Pierre-Louis Curien: A Model for Formal Parametric Polymorphism: A PER Interpretation for System R. 32-46
Stefano Berardi, Marc Bezem, Thierry Coquand: A realization of the negative interpretation of the Axiom of Choice. 47-62
Stefano Berardi, Luca Boerio: Using Subtyping in Program Optimization. 63-77
Gavin M. Bierman: What is a Categorical Model of Intuitionistic Linear Logic? 78-93
Daniel Briaud: An explicit Eta rewrite rule. 94-108
Yann Coscoy, Gilles Kahn, Laurent Théry: Extracting Text from Proofs. 109-123
Joëlle Despeyroux, Amy P. Felty, André Hirschowitz: Higher-Order Abstract Syntax in Coq. 124-138
Roberto Di Cosmo, Adolfo Piperno: Expanding Extensional Polymorphism. 139-153
Gilles Dowek: Lambda-calculus, Combinators and the Comprehension Scheme. 154-170
Neil Ghani: ßn-Equality for Coproducts. 171-185
Healfdene Goguen: Typed Operational Semantics. 186-200
Philippe de Groote: A Simple Calculus of Exception Handling. 201-215
Martin Hofmann: A Simple Model for Quotient Types. 216-234
M. Randall Holmes: Untyped lambda-Calculus with Relative Typing. 235-248
Furio Honsell, Marina Lenisa: Final Semantics for untyped lambda-calculus. 249-265
Antonius J. C. Hurkens: A Simplification of Girard's Paradox. 266-278
Hidetaka Kondoh: Basic Properties of Data Types with Inequational Refinements. 279-296
Toshihiko Kurata, Masako Takahashi: Decidable Properties of Intersection Type Systems. 297-311
François Leclerc: Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq. 312-327
Paul-André Melliès: Typed lambda-calculi with explicit substitutions may not terminate. 328-334
Vincent Padovani: On Equivalence Classes of Interpolation Equations. 335-349
Jaco van de Pol, Helmut Schwichtenberg: Strict Functionals for Termination Proofs. 350-364
Robert Pollack: A Verified Typechecker. 365-380
Alberto Pravato, Simona Ronchi Della Rocca, Luca Roversi: Categorical semantics of the call-by-value lambda-calculus. 381-396
Eike Ritter, Andrew M. Pitts: A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML. 397-413
Alex K. Simpson: Categorical completeness results for the simply-typed lambda-calculus. 414-427
Jan Springintveld: Third-Order Matching in the Presence of Type Constructors. 428-442