1 Search Results for "Kavvos, G. A."

Document
DOI: 10.4230/LIPIcs.ITP.2022.28
Deeper Shallow Embeddings

Authors: Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Deep and shallow embeddings are two popular techniques for embedding a language in a host language with complementary strengths and weaknesses. In a deep embedding, embedded constructs are defined as data in the host: this allows for syntax manipulation and facilitates metatheoretic reasoning, but is challenging to implement - especially in the case of dependently typed embedded languages. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them quite straightforward to implement, but limits their use in practice. In this paper, we attempt to bridge the gap between the two, by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.
Cite as

Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos. Deeper Shallow Embeddings. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28,
  author =	{Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
  title =	{{Deeper Shallow Embeddings}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.28},
  URN =		{urn:nbn:de:0030-drops-167379},
  doi =		{10.4230/LIPIcs.ITP.2022.28},
  annote =	{Keywords: type theory, shallow embedding, deep embedding, Agda}
}
  • Refine by Author
  • 1 Kavvos, G. A.
  • 1 Lampropoulos, Leonidas
  • 1 Prinz, Jacob

  • Refine by Classification
  • 1 Social and professional topics → History of programming languages
  • 1 Software and its engineering
  • 1 Software and its engineering → General programming languages

  • Refine by Keyword
  • 1 Agda
  • 1 deep embedding
  • 1 shallow embedding
  • 1 type theory

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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