Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications, TLCA '93, March 16-18, 1993, Utrecht, The Netherlands. ProceedingsThe lambda calculus was developed in the 1930s by Alonzo Church. The calculus turned out to be an interesting model of computation and became theprototype for untyped functional programming languages. Operational and denotational semantics for the calculus served as examples for otherprogramming languages. In typed lambda calculi, lambda terms are classified according to their applicative behavior. In the 1960s it was discovered that the types of typed lambda calculi are in fact appearances of logical propositions. Thus there are two possible views of typed lambda calculi: - as models of computation, where terms are viewed as programs in a typed programming language; - as logical theories, where the types are viewed as propositions and the terms as proofs. The practical spin-off from these studies are: - functional programming languages which are mathematically more succinct than imperative programs; - systems for automated proof checking based on lambda caluli. This volume is the proceedings of TLCA '93, the first international conference on Typed Lambda Calculi and Applications,organized by the Department of Philosophy of Utrecht University. It includes29 papers selected from 51 submissions. |
Contents
I | 1 |
II | 13 |
III | 29 |
IV | 45 |
V | 60 |
VI | 75 |
VII | 91 |
VIII | 107 |
XVII | 245 |
XVIII | 258 |
XIX | 274 |
XX | 289 |
XXI | 306 |
XXII | 318 |
XXIII | 328 |
XXIV | 346 |
IX | 124 |
X | 139 |
XI | 146 |
XII | 163 |
XIII | 179 |
XIV | 195 |
XV | 209 |
XVI | 230 |
XXV | 361 |
XXVI | 376 |
XXVII | 391 |
XXVIII | 406 |
XXIX | 418 |
XXX | |
Other editions - View all
Typed Lambda Calculi and Applications: International Conference on Typed ... Marc Bezem,Jan F. Groote No preview available - 2014 |
Common terms and phrases
algebra algorithm application arity axiom bool bound C-PCA Calculus of Constructions Church-Rosser combinatory complete lattice Computer Science confluence context critical pairs denotational semantics dependent type dependent type theory derivation DType elements elimination equivalence example exponential expression extended finite formulas free variables fully abstract given hence higher order induction hypothesis inductive definitions interpretation intersection types introduced judgements labels lambda calculus Lemma logical relations M₁ natural deduction natural numbers normal form normalizable notation obtained occur operation overloaded types parametricity polymorphic powerdomain predicate Programming Languages proof Proposition provable prove quantifiers recursive types redex result rewrite rule simply typed A-calculus strong normalization structure subset substitution subterm subtyping System F t₁ term rewriting systems Theorem topos tuple typable type assignment system type constructors type inference type system type theory type variables untyped well-typed X-terms