CoreFun: A typed functional reversible core language

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
Publication date2018
ISBN (Print)9783319994970
Publication statusPublished - 2018
Event10th International Conference on Reversible Computation, RC 2018 - Leicester, United Kingdom
Duration: 12 Sep 201814 Sep 2018


Conference10th International Conference on Reversible Computation, RC 2018
LandUnited Kingdom
SeriesLecture notes in computer science

    Research areas

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

ID: 203777951