Typed lambda calculi and applications. International conference, TLCA '93, March 16--18, 1993, Utrecht, the Netherlands. Proceedings (Q684571)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Akama, Yohji}, On Mints' reduction for ccc-calculus, 1-12 [Zbl 0786.03006] \textit{Altenkirch, Thorsten}, A formalization of the strong normalization proof for system F in LEGO, 13-28 [Zbl 0797.68095] \textit{van Bakel, Steffen}, Partial intersection type assignment in applicative term rewriting systems, 29-44 [Zbl 0797.68091] \textit{Barbanera, Franco; Berardi, Stefano}, Extracting constructive content from classical logic via control-like reductions, 45-59 [Zbl 0788.68016] \textit{Barbanera, Franco; Fernández, Maribel}, Combining first and higher order rewrite systems with type assignment systems, 60-74 [Zbl 0788.68079] \textit{Benton, Nick; Bierman, Gavin; de Paiva, Valeria; Hyland, Martin}, A term calculus for intuitionistic linear logic, 75-90 [Zbl 0795.68127] \textit{Berger, Ulrich}, Program extraction from normalization proofs, 91-106 [Zbl 0788.68015] \textit{Castagna, Giuseppe; Ghelli, Giorgio; Longo, Giuseppe}, A semantics for \(\lambda\)\&-\textit{early}: A calculus with overloading and early binding, 107-123 [Zbl 0797.68027] \textit{Di Gianantonio, Pietro; Honsell, Furio}, An abstract notion of application, 124-138 [Zbl 0788.68090] \textit{Dowek, Gilles}, The undecidability of typability in the lambda-pi-calculus, 139-145 [Zbl 0788.68017] \textit{Ghelli, Giorgio}, Recursive types are not conservative over \(F_ \leq\), 146-162 [Zbl 0786.03012] \textit{de Groote, Philippe}, The conservation theorem revisited, 163-178 [Zbl 0795.03020] \textit{Hyland, J. M. E.; Ong, C.-H. L.}, Modified realizability toposes and strong normalization proofs, 179-194 [Zbl 0793.03079] \textit{Jacobs, Bart}, Semantics of lambda-I and of other substructure lambda calculi, 195-208 [Zbl 0795.68126] \textit{Jacobs, Bart; Melham, Tom}, Translating dependent type theory into higher order logic, 209-229 [Zbl 0788.68130] \textit{Jung, Achim; Stoughton, Allen}, Studying the fully abstract model of PCF within its continuous function model, 230-244 [Zbl 0788.68021] \textit{Jung, Achim; Tiuryn, Jerzy}, A new characterization of lambda definability, 245-257 [Zbl 0795.03021] \textit{Leiß, Hans}, Combining recursive and dynamic types, 258-273 [Zbl 0795.68029] \textit{Leivant, Daniel; Marion, Jean-Yves}, Lambda calculus characterizations of poly-time, 274-288 [Zbl 0788.68051] \textit{McKinna, James; Pollack, Robert}, Pure type systems formalized, 289-305 [Zbl 0835.68068] \textit{Nipkow, Tobias}, Orthogonal higher-order rewrite systems are confluent, 306-317 [Zbl 0789.68081] \textit{Otth, Daniel F.}, Monotonic versus antimonotonic exponentiation, 318-327 [Zbl 0811.68104] \textit{Paulin-Mohring, Christine}, Inductive definitions in the system Coq; rules and properties, 328-345 [Zbl 0844.68073] \textit{Pierce, Benjamin C.}, Intersection types and bounded polymorphism, 346-360 [Zbl 0788.68022] \textit{Plotkin, Gordon; Abadi, Martín}, A logic for parametric polymorphism, 361-375 [Zbl 0788.68091] \textit{Sieber, Kurt}, Call-by-value and nondeterminism, 376-390 [Zbl 0788.68092] \textit{Springintveld, Jan}, Lower and upper bounds for reductions of types in \(\lambda{\underline \omega}\) and \(\lambda P\), 391-405 [Zbl 0795.68028] \textit{Takahashi, Masako}, \(\lambda\)-calculi with conditional rules, 406-417 [Zbl 0806.03014] \textit{Urzyczyn, Paweł}, Type reconstruction in \(\mathbf F_ \omega\) is undecidable, 418-432 [Zbl 0791.68059]