Monad translating inductive and coinductive types

Tarmo Uustalu*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Citations (Scopus)

Abstract

We show that the call-by-name monad translation of simply typed lambda calculus extended with sum and product types extends to special and general inductive and coinductive types so that its crucial property of preserving typings and β- and commuting reductions is maintained. Specific similar-purpose translations such as CPS translations follow from the general monad translations by specialization for appropriate concrete monads.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsHerman Geuvers, Freek Wiedijk
PublisherSpringer-Verlag
Pages299-315
Number of pages17
ISBN (Print)354014031X
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2646
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Monad translating inductive and coinductive types'. Together they form a unique fingerprint.

Cite this