License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.6
URN: urn:nbn:de:0030-drops-138853
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13885/
Go to the corresponding LIPIcs Volume Portal

Hondet, Gabriel ; Blanqui, Frédéric

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory

pdf-format:
LIPIcs-TYPES-2020-6.pdf (0.9 MB)

Abstract

The λΠ-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting.

BibTeX - Entry

@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6,
  author =	{Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13885},
  URN =		{urn:nbn:de:0030-drops-138853},
  doi =		{10.4230/LIPIcs.TYPES.2020.6},
  annote =	{Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance}
}

Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance
Collection: 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Issue Date: 2021
Date of publication: 07.06.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI