@inproceedings{4581a267e5304ce1a651eb2e60ef57d3,
title = "Turing-completeness totally free",
abstract = "In this paper, I show that general recursive definitions can be represented in the free monad which supports the {\textquoteleft}effect{\textquoteright} 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.",
keywords = "monad morphisms, total functional programming, monads, general recursion",
author = "Conor McBride",
year = "2015",
month = jun,
day = "9",
doi = "10.1007/978-3-319-19797-5_13",
language = "English",
isbn = "9783319197968",
volume = "9129",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "257--275",
editor = "Ralf Hinze and Janis Voigtl{\"a}nder",
booktitle = "Mathematics of Program Construction",
note = "12th International Conference on Mathematics of Program Construction (MPC 2015) ; Conference date: 29-06-2015 Through 01-07-2015",
}
