  This paper is concerned with the expressivity and denotational semantics of a
functional higher-order reversible programming language based on Theseus. In
this language, pattern-matching is used to ensure the reversibility of
functions. We show how one can encode any Reversible Turing Machine in said
language. We then build a sound and adequate categorical semantics based on
join inverse categories, with additional structures to capture
pattern-matching. We then derive a full completeness result, stating that any
computable, partial injective function is the image of a term in the language.

Logic in Computer Science