Loading...
Please wait, while we are loading the content...
Similar Documents
LF in LF: mechanizing the metatheories of LF in twelf
| Content Provider | ACM Digital Library |
|---|---|
| Author | Martens, Chris Crary, Karl |
| Abstract | We present a mechanized metatheoretic development of two presentations of LF: the Canonical presentation (in which only beta-short, eta-long terms are well-formed) and the original version based on definitional equivalence. We prove the standard metatheory, i.e. that type checking is decidable and canonical forms exist uniquely. We do so by translating structures from the original formulation to the canonical formulation, establishing that definitional equivalence corresponds to syntactic equivalence of canonical forms. This particular approach represents the first syntactic proof of the metatheory of LF, thus the first that can be mechanized in Twelf. It is also the first proof formally addressing the correspondence between hereditary substitution in Canonical LF and definitional equivalence in the traditional version, justifying the body of recent work that takes Canonical LF as primary. |
| Starting Page | 23 |
| Ending Page | 32 |
| Page Count | 10 |
| File Format | |
| ISBN | 9781450315784 |
| DOI | 10.1145/2364406.2364410 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2012-09-09 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Hereditary substitution Dependent type theory Logical frameworks Twelf Mechanized metatheory |
| Content Type | Text |
| Resource Type | Article |
