Programming type-safe transformations using higher-order abstract syntax

Autor: Olivier Savary Belanger, Stefan Monnier, Brigitte Pientka

Publikováno v: Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 49-91 (2015)

When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effo

Externí odkaz: https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Type-preserving CPS translation of Σ and Π types is not not possible

Autor: William J. Bowman, Nick Rioux, Amal Ahmed, Youyou Cong

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), pp.1-33. ⟨10.1145/3158110⟩
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), pp.1-33. ⟨10.1145/3158110⟩

Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass,

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::feace0e0b8a456e4c784de9fb4ea3671