×

Typed lambda calculi and applications. International conference, TLCA ’93, March 16–18, 1993, Utrecht, the Netherlands. Proceedings. (English) Zbl 0866.00038

Lecture Notes in Computer Science. 664. Berlin: Springer-Verlag. VIII, 433 p. DM 80.00 /sc (1993).

Show indexed articles as search result.

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

MSC:

00B25 Proceedings of conferences of miscellaneous specific interest
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03B40 Combinatory logic and lambda calculus

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI