Cakes That Bake Cakes: Dynamic Computation in CakeML

Autor: Sewell, T, Myreen, MO, Tan, YK, Kumar, R, Mihajlovic, A, Abrahamsson, O, Owens, S

We have extended the verified CakeML compiler with a new language primitive, Eval, which permits evaluation of new CakeML syntax at runtime. This new implementation supports an ambitious form of compilation at runtime and dynamic execution, where the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e6275dfc5020039b7f70d7d73a394232

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

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

Autor: Gross, Jason, Erbsen, Andres, Philipoom, Jade, Poddar-Agrawal, Miraya, Chlipala, Adam

Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1758a91f3c37beb0446a9b1c8f9b7c23
http://arxiv.org/abs/2205.00862

Verified code generation for the polyhedral model

Autor: Xavier Leroy, Nathanaël Courant

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩
Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩

International audience; The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::00125cb3020a5f3df5f17d92e4d1f3b1
https://doi.org/10.1145/3434321

Kalas: A Verified, End-To-End Compiler for a Choreographic Language

Autor: Pohjola, Johannes Åman, Gómez-Londoño, Alejandro, Shaker, James, Norrish, Michael

Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::443558e59ad8aaa141236d6ab88382d0