Loading...
Please wait, while we are loading the content...
Similar Documents
A Lambda Calculus Model of Martin-ll Of's Theory of Types with Explicit Substitution
| Content Provider | Semantic Scholar |
|---|---|
| Author | Fridlender, Daniel |
| Copyright Year | 1997 |
| Abstract | This paper presents a proof-irrelevant model of Martin-LL of's theory of types with explicit substitution; that is, a model in the style of Smi88], in which types are interpreted as truth values and objects (or proofs) are irrelevant. The fundamental diierence here is the need to cope with a formal system which in addition to types has sets and substitutions. This diierence leads us to a whole reformulation of the model which consists in deening an interpretation in terms of the untyped lambda calculus. From this interpretation the proof-irrelevant model is obtained as a particular instance. Finally, the paper outlines the deenition of a realizability model which is also obtained as a particular instance. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.chalmers.se/~frito/Papers/Model.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |