CoreFun: A typed functional reversible core language
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
CoreFun : A typed functional reversible core language. / Jacobsen, Petur Andrias Højgaard; Kaarsgaard, Robin; Thomsen, Michael Kirkedal.
Reversible Computation: 10th International Conference, RC 2018, 2018, Proceedings. Springer, 2018. p. 304-321 (Lecture notes in computer science, Vol. 11106).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - CoreFun
T2 - 10th International Conference on Reversible Computation, RC 2018
AU - Jacobsen, Petur Andrias Højgaard
AU - Kaarsgaard, Robin
AU - Thomsen, Michael Kirkedal
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
KW - Formal semantics
KW - Functional programming
KW - Programming languages
KW - Reversible computation
KW - Types
UR - http://www.scopus.com/inward/record.url?scp=85053514026&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-99498-7_21
DO - 10.1007/978-3-319-99498-7_21
M3 - Article in proceedings
AN - SCOPUS:85053514026
SN - 9783319994970
T3 - Lecture notes in computer science
SP - 304
EP - 321
BT - Reversible Computation
PB - Springer
Y2 - 12 September 2018 through 14 September 2018
ER -
ID: 203777951