Towards a formally verified proof assistant

Abhishek Anand; Vincent Rahli

doi:10.1007/978-3-319-08970-6_3

Towards a formally verified proof assistant

Abhishek Anand, Vincent Rahli

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

17 Citations (Scopus)

184 Downloads (Pure)

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.

Original language	English
Title of host publication	Interactive theorem proving
Subtitle of host publication	5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Editors	Gerwin Klein, Ruben Gamboa
Publisher	Springer
Pages	27-44
Volume	8558
ISBN (Electronic)	978-3-319-08970-6
ISBN (Print)	978-3-319-08969-0
DOIs	https://doi.org/10.1007/978-3-319-08970-6_3
Publication status	Published - Jul 2014
Event	International Conference on Interactive Theorem Proving - Vienna, Austria Duration: 14 Jul 2014 → 17 Jul 2014 Conference number: 5th

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Interactive Theorem Proving
Country/Territory	Austria
City	Vienna
Period	14/07/14 → 17/07/14
Other	5th 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

Access to Document

10.1007/978-3-319-08970-6_3Licence: None: All rights reserved

Anand_and_Rahli_Towards_a_Formally_Veried_Proof_Assistant_ITP_2014_Lecture_Notes_in_Computer_Science_vol_8558_Springer
This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science, vol 8558. The final authenticated version is available online at: http://dx.doi.org/10.1007/978-3-319-08970-6_3 Anand A., Rahli V. (2014) Towards a Formally Verified Proof Assistant. In: Klein G., Gamboa R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham
Accepted author manuscript, 493 KBLicence: None: All rights reserved

Cite this

Anand, A., & Rahli, V. (2014). Towards a formally verified proof assistant. In G. Klein, & R. Gamboa (Eds.), Interactive theorem proving : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Vol. 8558, pp. 27-44). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-08970-6_3

@inproceedings{de40a8b958e247ce8dc8ed86766bf2a4,

title = "Towards a formally verified proof assistant",

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) {\`a} la Allen. This type system includes Martin-L{\"o}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.",

keywords = "Type System, Type Theory, Partial Type, Dependent Type, Proof Assistant",

author = "Abhishek Anand and Vincent Rahli",

year = "2014",

month = jul,

doi = "10.1007/978-3-319-08970-6_3",

language = "English",

isbn = "978-3-319-08969-0",

volume = "8558",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "27--44",

editor = "Gerwin Klein and { Gamboa}, Ruben",

booktitle = "Interactive theorem proving",

note = "International Conference on Interactive Theorem Proving ; Conference date: 14-07-2014 Through 17-07-2014",

}

Anand, A & Rahli, V 2014, Towards a formally verified proof assistant. in G Klein & R Gamboa (eds), Interactive theorem proving : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. vol. 8558, Lecture Notes in Computer Science, Springer, pp. 27-44, International Conference on Interactive Theorem Proving, Vienna, Austria, 14/07/14. https://doi.org/10.1007/978-3-319-08970-6_3

Towards a formally verified proof assistant. / Anand, Abhishek; Rahli, Vincent.
Interactive theorem proving : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. ed. / Gerwin Klein; Ruben Gamboa. Vol. 8558 Springer, 2014. p. 27-44 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Towards a formally verified proof assistant

AU - Anand, Abhishek

AU - Rahli, Vincent

N1 - Conference code: 5th

PY - 2014/7

Y1 - 2014/7

N2 - 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.

AB - 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.

KW - Type System

KW - Type Theory

KW - Partial Type

KW - Dependent Type

KW - Proof Assistant

U2 - 10.1007/978-3-319-08970-6_3

DO - 10.1007/978-3-319-08970-6_3

M3 - Conference contribution

SN - 978-3-319-08969-0

VL - 8558

T3 - Lecture Notes in Computer Science

SP - 27

EP - 44

BT - Interactive theorem proving

A2 - Klein, Gerwin

A2 - Gamboa, Ruben

PB - Springer

T2 - International Conference on Interactive Theorem Proving

Y2 - 14 July 2014 through 17 July 2014

ER -

Anand A, Rahli V. Towards a formally verified proof assistant. In Klein G, Gamboa R, editors, Interactive theorem proving : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Vol. 8558. Springer. 2014. p. 27-44. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-08970-6_3

Towards a formally verified proof assistant

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this