Loading...
Please wait, while we are loading the content...
Similar Documents
A lambda calculus model of Martin-Löf's theory of types with explicit substitution (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Fridlender, Daniel |
| Description | This paper presents a proof-irrelevant model of Martin-Lof'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 difference here is the need to cope with a formal system which in addition to types has sets and substitutions. This difference leads us to a whole reformulation of the model which consists in defining 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 definition of a realizability model which is also obtained as a particular instance. Keywords: type theory, explicit substitution, models of type theory, proof-irrelevant model, realizability model. Contents 1 Introduction 1 2 Type theory 2 2.1 Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 3 A lambda calculus model 8 3.1 Semantic... |
| File Format | |
| Language | English |
| Publisher Date | 1997-01-01 |
| Publisher Institution | In this thesis |
| Access Restriction | Open |
| Subject Keyword | Explicit Substitution Realizability Model Truth Value Whole Reformulation Formal System Untyped Lambda Calculus Particular Instance Type Theory Proof-irrelevant Model Fundamental Difference Lambda Calculus Model |
| Content Type | Text |
| Resource Type | Article |
