Paper Info
Title
Proving Properties of Typed Lambda Terms: Realizability, Covers, and Sheaves (Abstract)
Abstract
We present a general method for proving properties of typed lambda terms. This method is obtained by introducing a semantic notion of realizability which uses the notion of a cover algebra (as in abstract sheaf theory). For this, we introduce a new class of semantic structures equipped with preorders, called preapplicative structures. In this framework, a general realizability theorem can be shown. Applying this theorem to the special case of the term model, yields a general theorem for proving properties of typed lambda terms, in particular, strong normalization and confluence. This approach clarifies the reducibility method by showing that the closure conditions on candidates of reducibility can be viewed as sheaf conditions.
Year
DOI
Venue
1993
10.1007/3-540-56868-9_11
RTA
Keywords
Field
DocType
typed lambda terms,proving properties
Discrete mathematics,Algebra,Typed lambda calculus,Pure mathematics,Mathematics,Realizability,Lambda
Conference
ISBN
Citations 
PageRank 
3-540-56868-9
0
0.34
References 
Authors
1
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86