A verified proof assistant

by Vincent Rahli, Abhishek Anand
2013

Abstract:

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
Time: 4-5pm
Location: Upson 5130

A verified proof assistant

by Vincent Rahli, Abhishek Anand 2013

by Vincent Rahli, Abhishek Anand
2013