Compilation of extended recursion in call-by-value functional languages
From MaRDI portal
Publication:848739
DOI10.1007/S10990-009-9042-ZzbMATH Open1183.68140arXiv0902.1257OpenAlexW3101389771MaRDI QIDQ848739FDOQ848739
Authors: Tom Hirschowitz, Xavier Leroy, J. B. Wells 
Publication date: 5 March 2010
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Abstract: This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than previous methods. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be correct.
Full work available at URL: https://arxiv.org/abs/0902.1257
Recommendations
- Optimizing structural recursion in functional programs
- Recursive Functions with Pattern Matching in Interaction Nets
- Algebraic correctness proofs for compiling recursive function definitions with strictness information
- Compilation and evaluation of linear mutual recursions
- Unraveling recursion: compiling an IR with recursion to System F
Cites Work
- Title not available (Why is that?)
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Compilation of extended recursion in call-by-value functional languages
- A syntactic approach to type soundness
- Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction
- Recursive monadic bindings
- Programming Languages and Systems
- Revised report on the algorithmic language scheme
- Addressed term rewriting systems: syntax, semantics, and pragmatics (extended abstract)
- Skew confluence and the lambda calculus with letrec
- The categorical abstract machine
- Fixing \texttt{letrec}: A faithful yet efficient implementation of Scheme's recursive binding construct
- A type system for well-founded recursion
- An abstract monadic semantics for value recursion
- The recursive record semantics of objects revisited
- A type system for recursive modules
- Recursive structures for standard ML
- Functional and Logic Programming
Cited In (13)
- Automatic generation of compiled forms for linear recursions
- Well-founded coalgebras, revisited
- Compilation and evaluation of linear mutual recursions
- Positive supercompilation for a higher-order call-by-value language
- Title not available (Why is that?)
- A sound strategy to compile general recursion into finite depth pattern matching
- Unraveling recursion: compiling an IR with recursion to System F
- Algebraic correctness proofs for compiling recursive function definitions with strictness information
- A mechanism of function calls in MSVL
- Compilation of extended recursion in call-by-value functional languages
- Title not available (Why is that?)
- An abstract monadic semantics for value recursion
- Fixing \texttt{letrec}: A faithful yet efficient implementation of Scheme's recursive binding construct
Uses Software
This page was built for publication: Compilation of extended recursion in call-by-value functional languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q848739)
