Towards a Formally Verified Proof Assistant

by Abhishek Anand, Vincent Rahli
2014

Presented at ITP 2014: International Conference on Interactive Theorem Proving, July 2014
Unofficial PDF
Corresponding technical report

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.

Towards a Formally Verified Proof Assistant

by Abhishek Anand, Vincent Rahli 2014

by Abhishek Anand, Vincent Rahli
2014