DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.26

Divide and Check: Logical Relations, No Algorithms Attached

Authors: Josselin Poiret, Kenji Maillard, and Nicolas Tabareau

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

The correctness of type-checking implementations for proof assistants based on dependent type theory relies on metatheoretical properties that ensure the decidability of typing, some of which require substantial logical strength. Recent mechanizations of such algorithms have highlighted the importance of separating the algorithmic components of the proof - often intricate but requiring relatively low logical strength - from the logical components, which depend on stronger metatheoretical properties, such as normalization or the injectivity of type constructors. In this work, we revisit the logical relations technique and show how it can be used to derive these metatheoretical properties in a direct and uniform way for a core dependent type theory featuring Π-types, N, ⊥ and a universe U. Our presentation yields a compact and conceptually simplified argument that isolates the logically strong reasoning from the algorithmic core. We argue that this approach scales smoothly to richer type theories, and demonstrate this by extending our construction to Exceptional Type Theory (ExcTT), obtaining the first mechanized canonicity proof for this theory.

Cite as

Josselin Poiret, Kenji Maillard, and Nicolas Tabareau. Divide and Check: Logical Relations, No Algorithms Attached. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{poiret_et_al:LIPIcs.FSCD.2026.26,
  author =	{Poiret, Josselin and Maillard, Kenji and Tabareau, Nicolas},
  title =	{{Divide and Check: Logical Relations, No Algorithms Attached}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{26:1--26:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.26},
  URN =		{urn:nbn:de:0030-drops-263764},
  doi =		{10.4230/LIPIcs.FSCD.2026.26},
  annote =	{Keywords: Type Theory, Proof Assistants}
}

Search Results

Documents authored by Poiret, Josselin

Divide and Check: Logical Relations, No Algorithms Attached

Abstract

Cite as

Thanks for your feedback!

Could not send message