<div dir="ltr"><div>Aloha Agda</div><div>FYI Work using Agda</div><div>Mahalo Agda</div><div><br></div><div>Art Scott</div><div><br></div><a href="https://arxiv.org/abs/2110.05404" target="_blank">https://arxiv.org/abs/2110.05404</a><div><br></div><div><br clear="all"><div>  • In Section 7, we show applications of our results to reversible circuits, using our formalisation.
Our results are stated using HoTT [Univalent Foundations Program 2013], and formalised using
the HoTT-Agda library (around 7,500 lines of code). Using the formalisation, we are able to
extract procedures for: (1) the synthesis of a reversible circuit from a permutation on a finite
set, (2) the verification that a reversible circuit realises a given permutation on finite sets, (3) a
normalisation-by-evaluation (NbE) procedure that reduces reversible circuits to canonical normal forms, (4) a sound and complete calculus for reasoning about reversible circuits and their
equivalences, and (5) the transfer of theorems about permutations and reversible circuits from
one representation to the other. </div><div><br></div><div>The proofs of some of our lemmas and propositions and theorems, as well as additional material,
are given in the supplementary appendices, and we refer to them in the text. Our accompanying
Agda code contains the formalisation of the full syntax, and most of our proofs.  <br></div><div><br></div><div><br></div><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div>Replace  <b style="background-color:rgb(255,0,0)"> HOT </b><span style="background-color:rgb(255,0,0)"> </span> computation with <span style="background-color:rgb(0,255,255)"><b><i>  COOL   </i></b></span> information</div><div>Harvest FREE sun. Free wind. Free storage. Free <i>Clean </i>Electrons of Freedom.</div><div>Peace, Love and Happiness<br>Only One Earth</div><div>Island Planet</div><div>Aloha spirit</div><div><img src="https://docs.google.com/uc?export=download&id=1gGxjdZZQNpaKr3ft3JIDH7PcXb6j90-w&revid=0B1DhFG-Fc1rsMENJL3hvbFhTY2FzZTNwRTVJSlFZYTNkSTl3PQ" width="91" height="96"><br></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>