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

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

Ejemplares similares