1 Search Results for "Mendes, Filipa"

Document
DOI: 10.4230/LIPIcs.FSCD.2023.19
The Logical Essence of Compiling with Continuations

Authors: José Espírito Santo and Filipa Mendes

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus (λ{𝖢}), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of λ{𝖢}, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.
Cite as

José Espírito Santo and Filipa Mendes. The Logical Essence of Compiling with Continuations. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 19:1-19:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2023.19,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Mendes, Filipa},
  title =	{{The Logical Essence of Compiling with Continuations}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{19:1--19:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.19},
  URN =		{urn:nbn:de:0030-drops-180036},
  doi =		{10.4230/LIPIcs.FSCD.2023.19},
  annote =	{Keywords: Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form}
}
  • Refine by Author
  • 1 Espírito Santo, José
  • 1 Mendes, Filipa

  • Refine by Classification
  • 1 Theory of computation → Operational semantics
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 1 Administrative normal form
  • 1 Continuation-passing style
  • 1 Generalized applications
  • 1 Sequent calculus

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact