2026-07-22T14:19:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4634 2024-03-06T10:35:10Z ddc:004 open_access

A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language Rodríguez, Leonardo Fridlender, Daniel Pagano, Miguel Abstract Machines Compiler Correctness Big-step semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leonardo Rodríguez and Daniel Fridlender and Miguel Pagano 2014 Is Part Of LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2013.230 urn:nbn:de:0030-drops-46343 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230 eng https://creativecommons.org/licenses/by/3.0/legalcode