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.FSCD.2022.25
URN: urn:nbn:de:0030-drops-163064
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16306/
Go to the corresponding LIPIcs Volume Portal

Felicissimo, Thiago

Adequate and Computational Encodings in the Logical Framework Dedukti

pdf-format:
LIPIcs-FSCD-2022-25.pdf (0.9 MB)

Abstract

Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.

BibTeX - Entry

@InProceedings{felicissimo:LIPIcs.FSCD.2022.25,
  author =	{Felicissimo, Thiago},
  title =	{{Adequate and Computational Encodings in the Logical Framework Dedukti}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16306},
  URN =		{urn:nbn:de:0030-drops-163064},
  doi =		{10.4230/LIPIcs.FSCD.2022.25},
  annote =	{Keywords: Type Theory, Logical Frameworks, Rewriting, Dedukti, Pure Type Systems}
}

Keywords: Type Theory, Logical Frameworks, Rewriting, Dedukti, Pure Type Systems
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022

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