Typed lambda calculi and applications. 2nd international conference, TLCA '95, Edinburgh, GB, April 10--12, 1995. Proceedings (Q1805041)

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 0866.00038]. Indexed articles: \textit{Asperti, Andrea; Laneve, Cosimo}, Comparing \(\lambda\)-calculus translations in sharing graphs, 1-15 [Zbl 1063.03507] \textit{Barthe, Gilles}, Extensions of pure type system, 16-31 [Zbl 1063.03508] \textit{Bellucci, Roberto; Abadi, Martín; Curien, Pierre-Louis}, A model for formal parametric polymorphism: a PER interpretation for system \(\mathcal R\)., 32-46 [Zbl 1063.03509] \textit{Berardi, Stefano; Bezem, Marc; Coquand, Thierry}, A realization of the negative interpretation of the axiom of choice, 47-62 [Zbl 1063.03537] \textit{Berardi, S.; Boerio, L.}, Using subtyping in program optimization, 63-77 [Zbl 1063.68562] \textit{Bierman, G. M.}, What is a categorical model of intuitionistic linear logic?, 78-93 [Zbl 1063.03534] \textit{Briaud, Daniel}, An explicit \(Eta\) rewrite rule, 94-108 [Zbl 1063.68552] \textit{Coscoy, Yann; Kahn, Gilles; Théry, Laurent}, Extracting text from proofs, 109-123 [Zbl 1063.68647] \textit{Desperyroux, Joëlle; Felty, Amy; Hirschowitz, André}, Higher-order abstract syntax in Coq, 124-138 [Zbl 1063.68650] \textit{Di Cosmo, Roberto; Piperno, Adolfo}, Expanding extensional polymorphism, 139-153 [Zbl 1063.68554] \textit{Dowek, Gilles}, Lambda-calculus, combinators and the comprehension scheme, 154-170 [Zbl 1063.03512] \textit{Ghani, Neil}, \(\beta\eta\)-equality for coproducts, 171-185 [Zbl 1063.03513] \textit{Goguen, Healfdene}, Typed operational semantics, 186-200 [Zbl 1063.68556] \textit{de Groote, Philippe}, A simple calculus of exception handling, 201-215 [Zbl 1063.68565] \textit{Hofmann, Martin}, A simple model for quotient types, 216-234 [Zbl 1063.68602] \textit{Holmes, M. Randall}, Untyped \(\lambda\)-calculus with relative typing, 235-248 [Zbl 1063.03515] \textit{Honsell, Furio; Lenisa, Marina}, Final semantics for untyped \(\lambda\)-calculus, 249-265 [Zbl 1063.03516] \textit{Hurkens, Antonius J. C.}, A simplification of Girard's paradox, 266-278 [Zbl 1063.03517] \textit{Kondoh, Hidetaka}, Basic properties of data types with inequational refinements (extended abstract), 279-296 [Zbl 1063.68606] \textit{Kurata, Toshihiko; Takahashi, Masako}, Decidable properties of intersection type systems, 297-311 [Zbl 1063.03519] \textit{Leclerc, François}, Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq, 312-327 [Zbl 1063.68656] \textit{Mellies, Paul-André}, Typed \(\lambda\)-calculi with explicit substitutions may not terminate, 328-334 [Zbl 1063.03522] \textit{Padovani, Vincent}, On equivalence classes of interpolation equations, 335-349 [Zbl 1063.03523] \textit{van de Pol, Jaco; Schwichtenberg, Helmut}, Strict functionals for termination proofs, 350-364 [Zbl 1063.03505] \textit{Pollack, Robert}, A verified typechecker, 365-380 [Zbl 1063.03502] \textit{Pravato, A.; Ronchi della Rocca, S.; Roversi, L.}, Categorical semantics of the call-by-value \(\lambda\)-calculus, 381-396 [Zbl 1063.68558] \textit{Ritter, Eike; Pitts, Andrew M.}, A fully abstract translation between a \(\lambda\)-calculus with reference types and standard ML., 397-413 [Zbl 1063.68551] \textit{Simpson, Alex K.}, Categorical completeness results for the simply-typed lambda-calculus, 414-427 [Zbl 1063.03524] \textit{Springintveld, Jan}, Third-order matching in the presence of type constructors (extended abstract), 428-442 [Zbl 1063.03525]