1 Search Results for "Rodríguez, Leonardo"

Document
DOI: 10.4230/LIPIcs.TYPES.2013.230
A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language

Authors: Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
In this paper we present a compiler that translates programs from an imperative higher-order language into a sequence of instructions for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is correct with respect to the big-step semantics of our language, both for convergent and divergent programs.
Cite as

Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230,
  author =	{Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel},
  title =	{{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{230--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230},
  URN =		{urn:nbn:de:0030-drops-46343},
  doi =		{10.4230/LIPIcs.TYPES.2013.230},
  annote =	{Keywords: Abstract Machines, Compiler Correctness, Big-step semantics}
}
  • Refine by Author
  • 1 Fridlender, Daniel
  • 1 Pagano, Miguel
  • 1 Rodríguez, Leonardo

  • Refine by Classification

  • Refine by Keyword
  • 1 Abstract Machines
  • 1 Big-step semantics
  • 1 Compiler Correctness

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2014

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