Towards a Formally Verified Proof Assistant (technical report)
Abhishek Anand, Vincent Rahli · Open Repository and Bibliography (University of Luxembourg) · 2014
This technical report describes our progress towards a formally verified version of the Nuprl Proof Assistant.We define a deep embedding of most of Nuprl into Coq.Among others, it includes a nominal-style definition of the Nuprl language, reduction rules, a coinductively defined computational equivalence, and the curry-style type system where types are defined as partial equivalence relations.Along with the core Martin-Löf dependent types, it includes Nuprl's hierarchy of universes, inductive types and partial types.This document is still a work in progress and may contain some mistakes.Please visit http://www.nuprl.org/html/verification/for the latest version.Definition compute step decide (arg1c:CanonicalOp) (t:NTerm) (arg1bts btsr : list BTerm) := match arg1c with | NInl ⇒ match (arg1bts, btsr ) with | ([bterm [] u] , [bterm [v1 ] t1 , bterm [v2 ] t2 ]) ⇒ csuccess (apply bterm (bterm [v1 ] t1 ) [u]) | ⇒ cfailure "bad argsto decide" t end | NInr ⇒ match (arg1bts, btsr ) with | ([bterm [] u] , [bterm [v1 ] t1 , bterm [v2 ] t2 ]) ⇒ csuccess (apply bterm (bterm [v2 ] t2 ) [u]) | ⇒ cfailure "inappropriate args to decide for Inr" t end | ⇒ cfailure "bad args to decide" t end. NCbvNCbv that is the call-by-value form of application.bterm [] (oterm (Can arg1c) arg1bts))::btsr ) Definition compute step cbv (arg1c:CanonicalOp) (t:NTerm) (arg1bts btsr : list BTerm) := match btsr with | [bterm [vs] t] ⇒ csuccess (apply bterm (bterm [vs] t) [(oterm (Can arg1c) arg1bts)]) | ⇒ cfailure "inappropriate args to cbv " t end.