Sökning: onr:"swepub:oai:research.chalmers.se:728d0fd0-d433-4589-b02c-c409368507b8" >
Automatically intro...
-
Abrahamsson, Oskar,1986Chalmers tekniska högskola,Chalmers University of Technology
(författare)
Automatically introducing tail recursion in CakeML
- Artikel/kapitelEngelska2018
Förlag, utgivningsår, omfång ...
-
2018-04-19
-
Cham :Springer International Publishing,2018
Nummerbeteckningar
-
LIBRIS-ID:oai:research.chalmers.se:728d0fd0-d433-4589-b02c-c409368507b8
-
https://research.chalmers.se/publication/503031URI
-
https://doi.org/10.1007/978-3-319-89719-6_7DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:kon swepub-publicationtype
-
Ämneskategori:ref swepub-contenttype
Anmärkningar
-
We describe and implement an optimizing compiler transformation which turns non–tail-recursive functions into equivalent tail-recursive functions in an intermediate language of the CakeML compiler. CakeML is a strongly typed functional language based on Standard ML with call-by-value semantics and a fully verified compiler. We integrate our implementation into CakeML compiler, and provide a machine-checked proof verifying that the observational semantics of programs is preserved under the transformation. To the best of our knowledge, this is the first fully verified implementation of this transformation in any modern compiler. Moreover, our verification efforts uncover surprising drawbacks in some of the verification techniques employed in several parts of the CakeML compiler. We provide a work-around for these drawbacks, and compare it to potential alternatives.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Myreen, Magnus,1983Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)myreen
(författare)
-
Chalmers tekniska högskola
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)Cham : Springer International Publishing10788, s. 118-1341611-33490302-9743
Internetlänk
Hitta via bibliotek
Till lärosätets databas