CoreFun: A Typed Functional Reversible Core Language

Petur Andrias Højgaard Jacobsen, Robin Kaarsgaard, Michael Kirkedal Thomsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


This paper presents CoreFun, a typed reversible functional language, which seeks to reduce typed reversible functional programming to its essentials. We present a complete formal definition of the language, including its formal semantics and type system, the latter of which is based on a combined reasoning logical system of unrestricted and relevantly typed terms, and allows special support for ancillary (read-only) variables through its unrestricted fragment. We show how, in many cases, the type system provides the possibility to statically check for the reversibility of programs. Finally, we detail how higher-level language features such as variants and type classes may be incorporated into CoreFun as syntactic sugar, such that CoreFun may be used as a core language for a reversible functional language in a more modern style.

Original languageEnglish
Title of host publicationReversible Computation - 10th International Conference, RC 2018, 2018, Proceedings
EditorsIrek Ulidowski, Jarkko Kari
Publication date2018
ISBN (Print)9783319994970
Publication statusPublished - 2018

Bibliographical note

DBLP's bibliographic metadata records provided through are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.


  • Formal semantics
  • Functional programming
  • Programming languages
  • Reversible computation
  • Types


Dive into the research topics of 'CoreFun: A Typed Functional Reversible Core Language'. Together they form a unique fingerprint.

Cite this