MSc by Petur Andrias Højgaard Jacobsen
Design of a Reversible Functional Programming Language -- And its Type System
Reversible programming languages are languages which exhibit both forward and backward determinism. The theory of reversible flowchart languages is relatively well understood, but studies of reversible functional languages are few and far between. In this thesis, we introduce a garbage-free, reversible, function language, inspired by RFun, which we call CoreFun.
We provide a formalization of its semantics and extend it with a type system based on relevance logic. The type system also has support for recursive and polymorphic types. With the type system, we are able to add the use of ancillae variables through an unrestricted fragment.
Finally, we describe how to lift the core language into a syntactically lighter language via a sequence of translation schemes, making it more amenable for modern style programming.
Advisors: Michael Kirkedal Thomsen and Robin Kaarsgaard (DIKU)
Examiners: Michael Kirkedal Thomsen (DIKU) and Mads Rosendahl (RUC)
All are welcome. No registration required.