1: \begin{abstract}

2: %   The reversible model of computation is motivated by the physical nature of computational processes and proposes

3: %   information-preserving computation. The primitive building blocks in this paradigm are reversible boolean gates, which

4: %   can also be formalised as permutations of sets of bits, or combinators for type isomorphisms. We unify these

5: %   approaches by giving a sound and complete denotational semantics for a first-order reversible programming language

6: %   $\PiLang$ for reversible circuits and circuit equivalences.

7: 

8: %   We establish a correspondence between $\PiLang$ and the groupoid of finite sets and bijections. The result suggests a

9: %   Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Monoidal

10: %   Groupoids. Using the formalisation of our result, we show how to perform normalisation, verification, and synthesis of

11: %   reversible and quantum circuits.

12: % \end{abstract}

13: