Towards a formally verified proof assistant

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

Standard

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 proceedingConference contribution

Harvard

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

APA

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

Vancouver

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). https://doi.org/10.1007/978-3-319-08970-6_3

Author

Anand, Abhishek ; Rahli, Vincent. / Towards a formally verified proof assistant. 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. editor / Gerwin Klein ; Ruben Gamboa. Vol. 8558 Springer, 2014. pp. 27-44 (Lecture Notes in Computer Science).

Bibtex

@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",

}

RIS

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 -