[Agda] Vikraman Choudhury, Jacek Karwowski, Amr Sabry --- results to reversible circuits...formalisation ... HoTT-Agda library (around 7, 500 lines of code) ... accompanying Agda code

[Art Scott]

Aloha Agda
FYI Work using Agda
Mahalo Agda

Art Scott

https://arxiv.org/abs/2110.05404


  • 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.

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.



-- 
Replace  * HOT *  computation with *  COOL   * information
Harvest FREE sun. Free wind. Free storage. Free *Clean *Electrons of
Freedom.
Peace, Love and Happiness
Only One Earth
Island Planet
Aloha spirit
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211228/29676aca/attachment.html>