A certified extension of the Krivine machine for a call-by-name higher-order imperative language
Fil: Rodríguez, Leonardo Matías. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
| Main Authors: | , , |
|---|---|
| Format: | publishedVersion |
| Language: | eng |
| Published: |
2022
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/30119 http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.230 |
| _version_ | 1801216011748245504 |
|---|---|
| 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 |
| collection | Repositorio Digital Universitario |
| description | Fil: Rodríguez, Leonardo Matías. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. |
| format | publishedVersion |
| id | rdu-unc.30119 |
| institution | Universidad Nacional de Cordoba |
| language | eng |
| publishDate | 2022 |
| record_format | dspace |
| spelling | rdu-unc.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 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. 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 |
| 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 |
| title | 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_short | 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 |
| topic | Abstract machines Compiler correctness Big-step semantics Algol like language Call by name Krivine machine |
| 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 |