A verified proof assistant
by Vincent Rahli, Abhishek Anand
We will discuss a project we started last summer which is an implementation of Nuprl in Coq, i.e., an implementation of Nuprl's computation system, and an implementation of Nuprl's PER semantics that was invented by Stuart Allen in the 80s.
This formal semantics allows us to prove that the inference rules of Nuprl are valid. Given an inference rule of the form: S1 /\ ... /\ Sn -> S, then proving that this rule is true amounts to proving that the truth of the sequents S1 ... Sn implies the truth of S. Such results give us a basis to build a verified version of Nuprl where these proofs are now our verified inference rules.
During this talk we will discuss the challenges of modeling a higher-order type theory into another, and of building a usable proof assistant on top of that model.
Date: October 30, 2013
Location: Upson 5130