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 [9]. 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.