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
Number of pages19
ISBN (Print)978-3-319-19796-8
StatePublished - 9 Jun 2015
Event12th International Conference on Mathematics of Program Construction (MPC 2015) - Königswinter, Germany
Duration: 29 Jun 20151 Jul 2015


Conference12th International Conference on Mathematics of Program Construction (MPC 2015)

    Research areas

  • monad morphisms, total functional programming, monads

View graph of relations