Search Results

Documents authored by Theocharis, Constantine

Artifact
Software
DOI: 10.4230/artifacts.26954
kontheocharis/erasure-impl

Authors: Constantine Theocharis

Abstract
Cite as

Constantine Theocharis. kontheocharis/erasure-impl (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26954,
   title = {{kontheocharis/erasure-impl}}, 
   author = {Theocharis, Constantine},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:18b74b13bf47b1740130031fe2cc393db1e95615;origin=https://github.com/kontheocharis/erasure-impl;visit=swh:1:snp:22f5796592ed642a59bdfc83787df0dd25d3d07e;anchor=swh:1:rev:b33efb7ac1b24535cdd4b1a6c13072f30ca9383b}{\texttt{swh:1:dir:18b74b13bf47b1740130031fe2cc393db1e95615}} (visited on 2026-07-15)},
   url = {https://github.com/kontheocharis/erasure-impl},
   doi = {10.4230/artifacts.26954},
}
Artifact
Software
DOI: 10.4230/artifacts.26955
kontheocharis/erasure-agda

Authors: Constantine Theocharis

Abstract
Cite as

Constantine Theocharis. kontheocharis/erasure-agda (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26955,
   title = {{kontheocharis/erasure-agda}}, 
   author = {Theocharis, Constantine},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:985bed7fde164c22db65b5fc19c69f7ad8896270;origin=https://github.com/kontheocharis/erasure-agda;visit=swh:1:snp:abe007c225313601adc0da7a9844de1a8cc993e0;anchor=swh:1:rev:b840465809e71c5fc469fcd8b267a8191e931341}{\texttt{swh:1:dir:985bed7fde164c22db65b5fc19c69f7ad8896270}} (visited on 2026-07-15)},
   url = {https://github.com/kontheocharis/erasure-agda},
   doi = {10.4230/artifacts.26955},
}
Document
DOI: 10.4230/LIPIcs.FSCD.2026.31
Type Theory with Erasure

Authors: Constantine Theocharis and Edwin Brady

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

Abstract
Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.
Cite as

Constantine Theocharis and Edwin Brady. Type Theory with Erasure. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{theocharis_et_al:LIPIcs.FSCD.2026.31,
  author =	{Theocharis, Constantine and Brady, Edwin},
  title =	{{Type Theory with Erasure}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{31:1--31:21},
  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.31},
  URN =		{urn:nbn:de:0030-drops-263816},
  doi =		{10.4230/LIPIcs.FSCD.2026.31},
  annote =	{Keywords: Type theory, erasure, dependent types, compilation, synthetic phase distinction, higher-order abstract syntax, logical frameworks}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact