A certified extension of the Krivine machine for a call-by-name higher-order imperative language

A certified extension of the Krivine machine for a call-by-name higher-order imperative language

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.

Saved in:
Bibliographic Details
Main Authors: Rodríguez, Leonardo Matías, Fridlender, Daniel Edgardo, Pagano, Miguel María
Format: article biblioteca
Language:eng
Published: 2014
Subjects:Abstract machines, Compiler correctness, Big-step semantics, Algol like language, Call by name, Krivine machine,
Online Access:http://hdl.handle.net/11086/30119
http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230
Tags: Add Tag
No Tags, Be the first to tag this record!
id dig-unc-ar-11086-30119
record_format koha
spelling dig-unc-ar-11086-301192022-12-30T09:38:27Z A certified extension of the Krivine machine for a call-by-name higher-order imperative language Rodríguez, Leonardo Matías Fridlender, Daniel Edgardo Pagano, Miguel María Abstract machines Compiler correctness Big-step semantics Algol like language Call by name Krivine machine 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. http://drops.dagstuhl.de/opus/volltexte/2014/4634 publishedVersion Fil: Rodríguez, Leonardo Matías. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Fridlender, Daniel Edgardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Pagano, Miguel María. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Ciencias de la Computación 2022-12-29T14:21:23Z 2022-12-29T14:21:23Z 2014 article http://hdl.handle.net/11086/30119 http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230 eng Attribution 3.0 Unported (CC BY 3.0) http://creativecommons.org/licenses/by/3.0/ Electrónico y/o Digital e-ISSN 1868-8969
institution UNC AR
collection DSpace
country Argentina
countrycode AR
component Bibliográfico
access En linea
databasecode dig-unc-ar
tag biblioteca
region America del Sur
libraryname Biblioteca 'Ing. Agrónomo Moisés Farber' de la Facultad de Ciencias Agropecuarias
language eng
topic Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
spellingShingle Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
Rodríguez, Leonardo Matías
Fridlender, Daniel Edgardo
Pagano, Miguel María
A certified extension of the Krivine machine for a call-by-name higher-order imperative language
description 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.
format article
topic_facet Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
author Rodríguez, Leonardo Matías
Fridlender, Daniel Edgardo
Pagano, Miguel María
author_facet Rodríguez, Leonardo Matías
Fridlender, Daniel Edgardo
Pagano, Miguel María
author_sort Rodríguez, Leonardo Matías
title A certified extension of the Krivine machine for a call-by-name higher-order imperative language
title_short A certified extension of the Krivine machine for a call-by-name higher-order imperative language
title_full A certified extension of the Krivine machine for a call-by-name higher-order imperative language
title_fullStr A certified extension of the Krivine machine for a call-by-name higher-order imperative language
title_full_unstemmed A certified extension of the Krivine machine for a call-by-name higher-order imperative language
title_sort certified extension of the krivine machine for a call-by-name higher-order imperative language
publishDate 2014
url http://hdl.handle.net/11086/30119
http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230
work_keys_str_mv AT rodriguezleonardomatias acertifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
AT fridlenderdanieledgardo acertifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
AT paganomiguelmaria acertifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
AT rodriguezleonardomatias certifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
AT fridlenderdanieledgardo certifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
AT paganomiguelmaria certifiedextensionofthekrivinemachineforacallbynamehigherorderimperativelanguage
_version_ 1756009604862443520

Similar Items