# * 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.