Name
Abstract | ||
|---|---|---|
It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step' form; but, once the correct form has been found, the proofs are very elegant and direct. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/11617990_1 | TYPES |
Keywords | Field | DocType |
pure type systems,binding constructor,formalized metatheory,careful thought,correct form,recent formalization,free variable,typing system,indexation,type system | Metatheory,Free variables and bound variables,Computer science,Indexed family,Algorithm,Type theory,Mathematical proof,Syntax | Conference |
Volume | ISSN | ISBN |
3839 | 0302-9743 | 3-540-31428-8 |
Citations | PageRank | References |
6 | 0.63 | 7 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Robin Adams | 1 | 60 | 11.61 |