Abstract
| Language | English |
|---|---|
| Title of host publication | Mathematics of Program Construction |
| Subtitle of host publication | 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings |
| Editors | Ralf Hinze, Janis Voigtländer |
| Place of Publication | Cham, Switzerland |
| Publisher | Springer |
| Pages | 257-275 |
| Number of pages | 19 |
| Volume | 9129 |
| ISBN (Print) | 9783319197968 |
| DOIs | |
| State | Published - 9 Jun 2015 |
| Event | 12th International Conference on Mathematics of Program Construction (MPC 2015) - Königswinter, Germany Duration: 29 Jun 2015 → 1 Jul 2015 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 9129 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 12th International Conference on Mathematics of Program Construction (MPC 2015) |
|---|---|
| Country | Germany |
| City | Königswinter |
| Period | 29/06/15 → 1/07/15 |
Fingerprint
Keywords
- monad morphisms
- total functional programming
- monads
- general recursion
Cite this
}
Turing-completeness totally free. / McBride, Conor.
Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings. ed. / Ralf Hinze; Janis Voigtländer. Vol. 9129 Cham, Switzerland : Springer, 2015. p. 257-275 (Lecture Notes in Computer Science; Vol. 9129).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Turing-completeness totally free
AU - McBride,Conor
PY - 2015/6/9
Y1 - 2015/6/9
N2 - 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.
AB - 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.
KW - monad morphisms
KW - total functional programming
KW - monads
KW - general recursion
UR - http://www.cs.ox.ac.uk/conferences/MPC2015/
U2 - 10.1007/978-3-319-19797-5_13
DO - 10.1007/978-3-319-19797-5_13
M3 - Conference contribution
SN - 9783319197968
VL - 9129
T3 - Lecture Notes in Computer Science
SP - 257
EP - 275
BT - Mathematics of Program Construction
PB - Springer
CY - Cham, Switzerland
ER -