Towards a formally verified proof assistant

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

Abstract

This paper presents a formalization of Nuprl's metatheory in Coq. It includes a nominal-style denition of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Currystyle type system where a type is dened 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.

Details

Original languageEnglish
Title of host publicationInteractive theorem proving
Subtitle of host publication5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
EditorsGerwin Klein, Ruben Gamboa
Publication statusPublished - Jul 2014
EventInternational Conference on Interactive Theorem Proving - Vienna, Austria
Duration: 14 Jul 201417 Jul 2014
Conference number: 5th

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Interactive Theorem Proving
Country/TerritoryAustria
CityVienna
Period14/07/1417/07/14
Other5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014

Keywords

  • Type System, Type Theory, Partial Type, Dependent Type, Proof Assistant