Loading...
Please wait, while we are loading the content...
Similar Documents
Towards observational type theory (2006)
| Content Provider | CiteSeerX |
|---|---|
| Author | Altenkirch, Thorsten Mcbride, Conor |
| Description | Observational Type Theory (OTT) combines beneficial aspects of Intensional and Extensional Type Theory (ITT/ETT). It separates definitional equality, decidable as in ITT, and a substitutive propositional equality, capturing extensional equality of functions, as in ETT. Moreover, canonicity holds: any closed term is definitionally reducible to a canonical value. Building on previous work by each author, this article reports substantial progress in the form of a simplified theory with a straightforward syntactic presentation, which we have implemented. As well as simplifying reasoning about functions, OTT offers potential foundational benefits, e.g. it gives rise to a closed type theory encoding inductive datatypes. 1. |
| File Format | |
| Language | English |
| Publisher Date | 2006-01-01 |
| Access Restriction | Open |
| Subject Keyword | Beneficial Aspect Previous Work Itt Ett Towards Observational Type Theory Extensional Type Theory Substitutive Propositional Equality Closed Type Theory Closed Term Observational Type Theory Potential Foundational Benefit Simplified Theory Extensional Equality Canonical Value Straightforward Syntactic Presentation Substantial Progress Definitional Equality Inductive Datatypes |
| Content Type | Text |
| Resource Type | Article |
