Theseus: a high level language for reversible computing. Programming in a reversible language remains “dierent” than programming in conventional irreversible languages, requiring specialized abstractions and unique modes of thinking. We present a high level language for reversible programming, called Theseus, that meshes naturally with conventional programming language abstractions. Theseus has the look and feel of a conventional functional language while maintaining a close correspondence with the low-level family of languages PI based on type isomorphisms . In contrast to the point-free combinators of PI. Theseus has variables and binding forms, algebraic data types, function definitions by pattern matching, and is Turing complete. The language is strongly typed and all well-typed programs are reversible. We explain the semantics of Theseus via a collection of progressively expressive examples and outline its correspondence to PI.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Paolini, Luca; Piccolo, Mauro; Roversi, Luca: A class of recursive permutations which is primitive recursive complete (2020)
- Kaarsgaard, Robin: Inversion, iteration, and the art of dual wielding (2019)
- Paolini, Luca; Piccolo, Mauro; Roversi, Luca: A certified study of a reversible programming language (2018)
- Kaarsgaard, Robin; Bock Axelsen, Holger; Glück, Robert: Join inverse categories and reversible recursion (2017)
- Axelsen, Holger Bock; Kaarsgaard, Robin: Join inverse categories as models of reversible recursion (2016)
- Carette, Jacques; Sabry, Amr: Computing with semirings and weak rig groupoids (2016)
- Schultz, Ulrik Pagh; Axelsen, Holger Bock: Elements of a reversible object-oriented language (work-in-progress report) (2016)
- Mogensen, Torben Ægidius: Garbage collection for reversible functional languages (2015)