L773:1611 3349 OR L773:0302 9743 OR L773:9783540433538
Search: L773:1611 3349 OR L773:0302 9743 OR L773:9783540433538 > (2015-2019) > Automatically intro...
- 6 of 357
- Previous record
- Next record
- To hitlist
Automatically introducing tail recursion in CakeML
-
- Abrahamsson, Oskar, 1986 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Myreen, Magnus, 1983 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
- (creator_code:org_t)
- 2018-04-19
- 2018
- English.
- In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10788, s. 118-134
- Conference paper (peer-reviewed)
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Språkteknologi (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Language Technology (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
- NATURVETENSKAP -- Matematik -- Matematisk analys (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Mathematical Analysis (hsv//eng)
Publication and Content Type
- kon (subject category)
- ref (subject category)
Find in a library
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artifici... (Search for host publication in LIBRIS)
To the university's database
- 6 of 357
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Abrahamsson, Osk ...
- Myreen, Magnus, ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Language Technol ...
-
- ENGINEERING AND TECHNOLOGY
- ENGINEERING AND ...
- and Electrical Engin ...
- and Computer Systems
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Mathematics
- and Mathematical Ana ...
- Articles in the publication
- Lecture Notes in ...
- By the university
- Chalmers University of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
