Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications, Tlca '93, March 16-18, 1993, Utrecht, the Ne

ISBN-13: 9783540565178 / Angielski / Miękka / 1993 / 443 str.

Marc Bezem; Jan F. Groote; M. Bezem

Opis

This volume of conference proceedings contains 29 research papers on typed lambda calculi, which are used as models of computation (where terms are viewed as programs in a typed programming language) and as logical theories (where types are viewed as propositions and terms as proofs).

Spis treści

On Mints' reduction for ccc-calculus.- A formalization of the strong normalization proof for System F in LEGO.- Partial intersection type assignment in applicative term rewriting systems.- Extracting constructive content from classical logic via control-like reductions.- Combining first and higher order rewrite systems with type assignment systems.- A term calculus for Intuitionistic Linear Logic.- Program extraction from normalization proofs.- A semantics for ? &-early: a calculus with overloading and early binding.- An abstract notion of application.- The undecidability of typability in the Lambda-Pi-calculus.- Recursive types are not conservative over F?.- The conservation theorem revisited.- Modified realizability toposes and strong normalization proofs.- Semantics of lambda-I and of other substructure lambda calculi.- Translating dependent type theory into higher order logic.- Studying the fully abstract model of PCF within its continuous function model.- A new characterization of lambda definability.- Combining recursive and dynamic types.- Lambda calculus characterizations of poly-time.- Pure type systems formalized.- Orthogonal higher-order rewrite systems are confluent.- Monotonic versus antimonotonic exponentiation.- Inductive definitions in the system Coq rules and properties.- Intersection types and bounded polymorphism.- A logic for parametric polymorphism.- Call-by-value and nondeterminism.- Lower and upper bounds for reductions of types in ? and ?P (extended abstract).- ?-Calculi with conditional rules.- Type reconstruction in F? is undecidable.