Name
Abstract | ||
|---|---|---|
In this paper, I show that general recursive definitions can be represented in the free monad which supports the 'effect' of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-19797-5_13 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Discrete mathematics,Programming language,Total functional programming,Turing completeness,Computer science,Theoretical computer science,Agda,Morphism,Monad (functional programming),Recursion,Semantics,Recursive definition | Conference | 9129 |
ISSN | Citations | PageRank |
0302-9743 | 7 | 0.44 |
References | Authors | |
16 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Conor McBride | 1 | 752 | 47.89 |