Abstract
This paper presents a formalization of Nuprl's metatheory in Coq. It includes a nominal-style definition of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Curry-style type system where a type is defined as a Partial Equivalence Relation (PER) à la Allen. This type system includes Martin-Löf dependent types, a hierarchy of universes, inductive types and partial types. We then prove that the typehood rules of Nuprl are valid w.r.t. this PER semantics and hence reduce Nuprl's consistency to Coq's consistency. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Anand, A., & Rahli, V. (2014). Towards a formally verified proof assistant. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 27–44). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
