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. Backwards determinism of of branching is achieved with a First Match Policy, but we investigate the possibility of ensuring backwards determinism with exit assertions or static guarantees of orthogonality as alternatives. As program inversion of non-flowchart languages generally is hard, we present a formalization of its inverse semantics instead. 

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.