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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Rodríguez, Leonardo Matías, Fridlender, Daniel Edgardo, Pagano, Miguel María
Formato: article
Lenguaje:Inglés
Publicado: 2022
Materias:
Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
Acceso en línea:http://hdl.handle.net/11086/30119
http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-30119
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic 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
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
topic_facet Abstract machines
Compiler correctness
Big-step semantics
Algol like language
Call by name
Krivine machine
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
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 2022
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
bdutipo_str Repositorios
_version_ 1764820393034514433

Ejemplares similares