Turing-completeness totally free

Research output: ResearchConference contribution

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.
Original languageEnglish
Title of host publicationMathematics of Program Construction
Subtitle of host publication12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings
EditorsRalf Hinze, Janis Voigtländer
Place of PublicationCham, Switzerland
PublisherSpringer
Pages257-275
Number of pages19
Volume9129
ISBN (Print)978-3-319-19796-8
DOIs
StatePublished - 9 Jun 2015
Event12th International Conference on Mathematics of Program Construction (MPC 2015) - Königswinter, Germany
Duration: 29 Jun 20151 Jul 2015

Conference

Conference12th International Conference on Mathematics of Program Construction (MPC 2015)
CountryGermany
CityKönigswinter
Period29/06/151/07/15

    Research areas

  • monad morphisms, total functional programming, monads

View graph of relations