Typed Lambda Calculi and Applications
International Conference on Typed Lambda Calculi and Applications, TLCA '93, March 1618, 1993, Utrecht, The Netherlands. Proceedings
Editors: Bezem, Marc, Groote, Jan F. (Eds.)
Free PreviewBuy this book
 About this book

The 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 spinoff 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.
 Table of contents (29 chapters)


On Mints' reduction for ccccalculus
Pages 112

A formalization of the strong normalization proof for System F in LEGO
Pages 1328

Partial intersection type assignment in applicative term rewriting systems
Pages 2944

Extracting constructive content from classical logic via controllike reductions
Pages 4559

Combining first and higher order rewrite systems with type assignment systems
Pages 6074

Table of contents (29 chapters)
Recommended for you
Bibliographic Information
 Bibliographic Information

 Book Title
 Typed Lambda Calculi and Applications
 Book Subtitle
 International Conference on Typed Lambda Calculi and Applications, TLCA '93, March 1618, 1993, Utrecht, The Netherlands. Proceedings
 Editors

 Marc Bezem
 Jan F. Groote
 Series Title
 Lecture Notes in Computer Science
 Series Volume
 664
 Copyright
 1993
 Publisher
 SpringerVerlag Berlin Heidelberg
 Copyright Holder
 SpringerVerlag Berlin Heidelberg
 eBook ISBN
 9783540475866
 DOI
 10.1007/BFb0037093
 Softcover ISBN
 9783540565178
 Series ISSN
 03029743
 Edition Number
 1
 Number of Pages
 IX, 443
 Topics