2dtypesZot.bib

@inproceedings{aaronsonClassificationReversibleBit2017,
  title = {The {{Classification}} of {{Reversible Bit Operations}}},
  booktitle = {8th {{Innovations}} in {{Theoretical Computer Science Conference}} ({{ITCS}} 2017)},
  author = {Aaronson, Scott and Grier, Daniel and Schaeffer, Luke},
  editor = {Papadimitriou, Christos H.},
  year = {2017},
  series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})},
  volume = {67},
  pages = {23:1--23:34},
  publisher = {{Schloss Dagstuhl\textendash Leibniz-Zentrum fuer Informatik}},
  address = {{Dagstuhl, Germany}},
  issn = {1868-8969},
  doi = {10.4230/LIPIcs.ITCS.2017.23},
  url = {http://drops.dagstuhl.de/opus/volltexte/2017/8173},
  urldate = {2021-11-10},
  isbn = {978-3-95977-029-3},
  keywords = {Boolean logic,Circuit synthesis,Gate classification,Post’s lattice,Reversible computation,Reversible gates}
}

@inproceedings{abramskyAbstractScalarsLoops2005,
  title = {Abstract {{Scalars}}, {{Loops}}, and {{Free Traced}} and {{Strongly Compact Closed Categories}}},
  booktitle = {Algebra and {{Coalgebra}} in {{Computer Science}}},
  author = {Abramsky, Samson},
  editor = {Fiadeiro, Jos{\'e} Luiz and Harman, Neil and Roggenbach, Markus and Rutten, Jan},
  year = {2005},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {1--29},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/11548133_1},
  url = {10.1007/11548133_1},
  abstract = {We study structures which have arisen in recent work by the present author and Bob Coecke on a categorical axiomatics for Quantum Mechanics; in particular, the notion of strongly compact closed category. We explain how these structures support a notion of scalar which allows quantitative aspects of physical theory to be expressed, and how the notion of strong compact closure emerges as a significant refinement of the more classical notion of compact closed category.We then proceed to an extended discussion of free constructions for a sequence of progressively more complex kinds of structured category, culminating in the strongly compact closed case. The simple geometric and combinatorial ideas underlying these constructions are emphasized. We also discuss variations where a prescribed monoid of scalars can be `glued in' to the free construction.},
  isbn = {978-3-540-31876-7},
  langid = {english},
  keywords = {Algebraic Description,Monoidal Category,Monoidal Structure,Symmetric Monoidal Category,Tensor Product},
  annotation = {ZSCC: NoCitationData[s1]}
}

@article{abramskyStructuralApproachReversible2005,
  title = {A Structural Approach to Reversible Computation},
  author = {Abramsky, Samson},
  year = {2005},
  month = dec,
  journal = {Theoretical Computer Science},
  volume = {347},
  number = {3},
  pages = {441--464},
  issn = {03043975},
  doi = {10.1016/j.tcs.2005.07.002},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0304397505003804},
  urldate = {2021-11-10},
  abstract = {Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic\textemdash but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.},
  langid = {english}
}

@misc{aleksandrowiczQiskitOpensourceFramework2019,
  title = {Qiskit: An {{Open}}-Source {{Framework}} for {{Quantum Computing}}},
  shorttitle = {Qiskit},
  author = {Aleksandrowicz, Gadi and Alexander, Thomas and Barkoutsos, Panagiotis and Bello, Luciano and {Ben-Haim}, Yael and Bucher, David and {Cabrera-Hern{\'a}ndez}, Francisco Jose and {Carballo-Franquis}, Jorge and Chen, Adrian and Chen, Chun-Fu and Chow, Jerry M. and {C{\'o}rcoles-Gonzales}, Antonio D. and Cross, Abigail J. and Cross, Andrew and {Cruz-Benito}, Juan and Culver, Chris and Gonz{\'a}lez, Salvador De La Puente and Torre, Enrique De La and Ding, Delton and Dumitrescu, Eugene and Duran, Ivan and Eendebak, Pieter and Everitt, Mark and Sertage, Ismael Faro and Frisch, Albert and Fuhrer, Andreas and Gambetta, Jay and Gago, Borja Godoy and {Gomez-Mosquera}, Juan and Greenberg, Donny and Hamamura, Ikko and Havlicek, Vojtech and Hellmers, Joe and {\L}ukasz Herok and Horii, Hiroshi and Shaohan Hu and Imamichi, Takashi and Toshinari Itoko and {Javadi-Abhari}, Ali and Kanazawa, Naoki and Karazeev, Anton and Krsulich, Kevin and Liu, Peng and Luh, Yang and Yunho Maeng and Marques, Manoel and {Mart{\'i}n-Fern{\'a}ndez}, Francisco Jose and McClure, Douglas T. and McKay, David and Srujan Meesala and Mezzacapo, Antonio and Moll, Nikolaj and Rodr{\'i}guez, Diego Moreda and Nannicini, Giacomo and Nation, Paul and Ollitrault, Pauline and O'Riordan, Lee James and Hanhee Paik and P{\'e}rez, Jes{\'u}s and Phan, Anna and Pistoia, Marco and Prutyanov, Viktor and Reuter, Max and Rice, Julia and Abd{\'o}n Rodr{\'i}guez Davila and Rudy, Raymond Harry Putra and Mingi Ryu and Ninad Sathaye and Schnabel, Chris and Schoute, Eddie and Kanav Setia and Yunong Shi and Adenilton Silva and Siraichi, Yukio and Seyon Sivarajah and Smolin, John A. and Soeken, Mathias and Takahashi, Hitomi and Tavernelli, Ivano and Taylor, Charles and Taylour, Pete and Kenso Trabing and Treinish, Matthew and Turner, Wes and {Vogt-Lee}, Desiree and Vuillot, Christophe and Wildstrom, Jonathan A. and Wilson, Jessica and Winston, Erick and Wood, Christopher and Wood, Stephen and W{\"o}rner, Stefan and Akhalwaya, Ismail Yunus and Zoufal, Christa},
  year = {2019},
  month = jan,
  doi = {10.5281/ZENODO.2562110},
  url = {https://zenodo.org/record/2562110},
  urldate = {2021-07-09},
  abstract = {Qiskit is an open-source framework for working with noisy quantum computers at the level of pulses, circuits, and algorithms. https://qiskit.org},
  copyright = {Apache License 2.0, Open Access},
  howpublished = {Zenodo},
  langid = {english},
  keywords = {qiskit,quantum computing,quantum programming language,sdk},
  annotation = {ZSCC: NoCitationData[s0]}
}

@phdthesis{angiuliComputationalSemanticsCartesianCubical2019,
  title = {Computational {{Semantics}} of {{CartesianCubical Type Theory}}},
  author = {Angiuli, Carlo},
  year = {2019},
  month = sep,
  address = {{Pittsburgh, PA}},
  url = {https://www.cs.cmu.edu/~cangiuli/thesis/thesis.pdf},
  school = {Carnegie Mellon University},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{angiuliInternalizingRepresentationIndependence2021,
  title = {Internalizing Representation Independence with Univalence},
  author = {Angiuli, Carlo and Cavallo, Evan and M{\"o}rtberg, Anders and Zeuner, Max},
  year = {2021},
  month = jan,
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  pages = {12:1--12:30},
  doi = {10.1145/3434293},
  url = {https://doi.org/10.1145/3434293},
  urldate = {2021-07-09},
  abstract = {In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.},
  keywords = {Cubical Type Theory,Higher Inductive Types,Proof Assistants,Representation Independence,Univalence},
  annotation = {ZSCC: 0000007}
}

@article{baezCategoriesNets2021,
  title = {Categories of {{Nets}}},
  author = {Baez, John C. and Genovese, Fabrizio and Master, Jade and Shulman, Michael},
  year = {2021},
  month = apr,
  journal = {arXiv:2101.04238 [cs, math]},
  eprint = {2101.04238},
  eprinttype = {arxiv},
  primaryclass = {cs, math},
  url = {http://arxiv.org/abs/2101.04238},
  urldate = {2021-06-29},
  abstract = {We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we call \$\textbackslash Sigma\$-nets, which allow finer control over whether tokens are treated using the collective or individual token philosophy. We describe three forms of execution semantics in which pre-nets generate strict monoidal categories, \$\textbackslash Sigma\$-nets (including whole-grain Petri nets) generate symmetric strict monoidal categories, and Petri nets generate commutative monoidal categories, all by left adjoint functors. We also construct adjunctions relating these categories of nets to each other, in particular showing that all kinds of net can be embedded in the unifying category of \$\textbackslash Sigma\$-nets, in a way that commutes coherently with their execution semantics.},
  archiveprefix = {arXiv},
  keywords = {⛔ No DOI found,Computer Science - Formal Languages and Automata Theory,Mathematics - Category Theory},
  annotation = {ZSCC: 0000004}
}

@incollection{baezFiniteSetsFeynman2001,
  title = {From {{Finite Sets}} to {{Feynman Diagrams}}},
  booktitle = {Mathematics {{Unlimited}} \textemdash{} 2001 and {{Beyond}}},
  author = {Baez, John C. and Dolan, James},
  editor = {Engquist, Bj{\"o}rn and Schmid, Wilfried},
  year = {2001},
  pages = {29--50},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/978-3-642-56478-9_3},
  url = {https://doi.org/10.1007/978-3-642-56478-9_3},
  urldate = {2021-11-10},
  abstract = {Prediction is hard, especially when it comes to the future, but barring some unforeseen catastrophe, we can expect the amount of mathematics produced in the 21st century to dwarf that of all the centuries that came before. By the very nature of its subject matter, mathematics is capable of limitless expansion. Thanks to rapid improvements in technology, our computational power is in a phase of exponential growth. Even if this growth slows, we have barely begun to exploit our new abilities. Thus the interesting question is not whether the 21st century will see an unprecedented explosion of new mathematics. It is whether anyone will ever understand more than the tiniest fraction of this new mathematics \textemdash{} or even the mathematics we already have.},
  isbn = {978-3-642-56478-9},
  langid = {english}
}

@article{baezHIGHERDIMENSIONALALGEBRA2010,
  title = {{{HIGHER DIMENSIONAL ALGEBRA VII}}: {{GROUPOIDIFICATION}}},
  author = {Baez, John C and Hoffnung, Alexander E and Walker, Christopher D},
  year = {2010},
  journal = {Theory and Applications of Categories},
  volume = {24},
  pages = {66},
  url = {http://www.tac.mta.ca/tac/volumes/24/18/24-18abs.html},
  abstract = {Groupoidification is a form of categorification in which vector spaces are replaced by groupoids and linear operators are replaced by spans of groupoids. We introduce this idea with a detailed exposition of `degroupoidification': a systematic process that turns groupoids and spans into vector spaces and linear operators. Then we present three applications of groupoidification. The first is to Feynman diagrams. The Hilbert space for the quantum harmonic oscillator arises naturally from degroupoidifying the groupoid of finite sets and bijections. This allows for a purely combinatorial interpretation of creation and annihilation operators, their commutation relations, field operators, their normal-ordered powers, and finally Feynman diagrams. The second application is to Hecke algebras. We explain how to groupoidify the Hecke algebra associated to a Dynkin diagram whenever the deformation parameter q is a prime power. We illustrate this with the simplest nontrivial example, coming from the A2 Dynkin diagram. In this example we show that the solution of the Yang\textendash Baxter equation built into the A2 Hecke algebra arises naturally from the axioms of projective geometry applied to the projective plane over the finite field Fq. The third application is to Hall algebras. We explain how the standard construction of the Hall algebra from the category of Fq representations of a simply-laced quiver can be seen as an example of degroupoidification. This in turn provides a new way to categorify\textemdash or more precisely, groupoidify\textemdash the positive part of the quantum group associated to the quiver.},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000054}
}

@article{bakerLivelyLinearLisp1992,
  title = {Lively Linear {{Lisp}}: ``Look Ma, No Garbage!''},
  shorttitle = {Lively Linear {{Lisp}}},
  author = {Baker, Henry G.},
  year = {1992},
  month = aug,
  journal = {ACM SIGPLAN Notices},
  volume = {27},
  number = {8},
  pages = {89--98},
  issn = {0362-1340},
  doi = {10.1145/142137.142162},
  url = {https://doi.org/10.1145/142137.142162},
  urldate = {2021-11-10},
  abstract = {Linear logic has been proposed as one solution to the problem of garbage collection and providing efficient "update-in-place" capabilities within a more functional language. Linear logic conserves accessibility, and hence provides a mechanical metaphor which is more appropriate for a distributed-memory parallel processor in which copying is explicit. However, linear logic's lack of sharing may introduce significant inefficiencies of its own.We show an efficient implementation of linear logic called Linear Lisp that runs within a constant factor of non-linear logic. This Linear Lisp allows RPLACX operations, and manages storage as safely as a non-linear Lisp, but does not need a garbage collector. Since it offers assignments but no sharing, it occupies a twilight zone between functional languages and imperative languages. Our Linear Lisp Machine offers many of the same capabilities as combinator/graph reduction machines, but without their copying and garbage collection problems.}
}

@inproceedings{bakerNREVERSALFortuneThermodynamics1992,
  title = {{{NREVERSAL}} of Fortune \textemdash{} {{The}} Thermodynamics of Garbage Collection},
  booktitle = {Memory {{Management}}},
  author = {Baker, Henry G.},
  editor = {Bekkers, Yves and Cohen, Jacques},
  year = {1992},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {507--524},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/BFb0017210},
  abstract = {The need to reverse a computation arises in many contexts\textemdash debugging, editor undoing, optimistic concurrency undoing, speculative computation undoing, trace scheduling, exception handling undoing, database recovery, optimistic discrete event simulations, subjunctive computing, etc. The need to analyze a reversed computation arises in the context of static analysis\textemdash liveness analysis, strictness analysis, type inference, etc. Traditional means for restoring a computation to a previous state involve checkpoints; checkpoints require time to copy, as well as space to store, the copied material. Traditional reverse abstract interpretation produces relatively poor information due to its inability to guess the previous values of assigned-to variables.We propose an abstract computer model and a programming language\textemdash{$\Psi$}-Lisp\textemdash whose primitive operations are injective and hence reversible, thus allowing arbitrary undoing without the overheads of checkpointing. Such a computer can be built from reversible conservative logic circuits, with the serendipitous advantage of dissipating far less heat than traditional Boolean AND/OR/NOT circuits. Unlike functional languages, which have one ``state'' for all times, {$\Psi$}-Lisp has at all times one ``state'', with unique predecessor and successor states.Compiling into a reversible pseudocode can have benefits even when targeting a traditional computer. Certain optimizations, e.g., update-in-place, and compile-time garbage collection may be more easily performed, because the information may be elicited without the difficult and time-consuming iterative abstract interpretation required for most non-reversible models.In a reversible machine, garbage collection for recycling storage can always be performed by a reversed (sub)computation. While this ``collection is reversed mutation'' insight does not reduce space requirements when used for the computation as a whole, it does save space when used to recycle at finer scales. This insight also provides an explanation for the fundamental importance of the push-down stack both for recognizing palindromes and for managing storage.Reversible computers are related to Prolog, linear logic and chemical abstract machines.},
  isbn = {978-3-540-47315-2},
  langid = {english},
  keywords = {Functional Language,Garbage Collection,Garbage Collector,Lambda Calculus,Reversible Computer}
}

@article{beauregardCircuitShorAlgorithm2003,
  title = {Circuit for {{Shor}}'s Algorithm Using 2n+3 Qubits},
  author = {Beauregard, Stephane},
  year = {2003},
  month = mar,
  journal = {Quantum Information \& Computation},
  volume = {3},
  number = {2},
  pages = {175--185},
  issn = {1533-7146},
  abstract = {We try to minimize the number of qubits needed to factor an integer of n bits using Shor's algorithm on a quantum computer. We introduce a circuit which uses 2n + 3 qubits and 0(n3lg(n)) elementary quantum gates in a depth of 0(n3) to implement the factorization algorithm. The circuit is computable in polynomial time on a classical computer and is completely general as it does not rely on any property of the number to be factored.},
  keywords = {factorization,modular arithmetics,quantum circuits}
}

@article{bekeCategorificationTermRewriting2011,
  title = {Categorification, Term Rewriting and the {{Knuth}}\textendash{{Bendix}} Procedure},
  author = {Beke, Tibor},
  year = {2011},
  month = may,
  journal = {Journal of Pure and Applied Algebra},
  volume = {215},
  number = {5},
  pages = {728--740},
  issn = {0022-4049},
  doi = {10.1016/j.jpaa.2010.06.019},
  url = {10.1016/j.jpaa.2010.06.019},
  urldate = {2021-06-28},
  abstract = {An axiomatization of a finitary, equational universal algebra by a convergent term rewrite system gives rise to a finite, coherent categorification of the algebra.},
  langid = {english},
  annotation = {ZSCC: 0000004}
}

@book{bellmanCombinatorialAnalysis1960,
  title = {Combinatorial {{Analysis}}},
  author = {Bellman, Richard and Hall, Marshall},
  year = {1960},
  series = {Proceedings of {{Symposia}} in {{Applied Mathematics}}},
  volume = {10},
  publisher = {{American Mathematical Society}},
  issn = {2324-7088, 0160-7634},
  doi = {http://dx.doi.org/10.1090/psapm/010},
  url = {https://doi.org/10.1090/psapm/010},
  urldate = {2021-01-30},
  abstract = {Advancing research. Creating connections.},
  isbn = {978-0-8218-1310-2 978-0-8218-7334-2 978-0-8218-9225-1},
  langid = {english},
  annotation = {ZSCC: 0000000}
}

@article{bennettFundamentalPhysicalLimits1985,
  title = {The {{Fundamental Physical Limits}} of {{Computation}}},
  author = {Bennett, Charles H. and Landauer, Rolf},
  year = {1985},
  journal = {Scientific American},
  volume = {253},
  number = {1},
  pages = {48--57},
  publisher = {{Scientific American, a division of Nature America, Inc.}},
  issn = {0036-8733},
  url = {https://www.jstor.org/stable/24967723},
  urldate = {2021-11-10}
}

@article{bergerTeachingOrdinalPatterns2019,
  title = {Teaching {{Ordinal Patterns}} to a {{Computer}}: Efficient {{Encoding Algorithms Based}} on the {{Lehmer Code}}},
  shorttitle = {Teaching {{Ordinal Patterns}} to a {{Computer}}},
  author = {Berger, Sebastian and Kravtsiv, Andrii and Schneider, Gerhard and Jordan, Denis},
  year = {2019},
  month = oct,
  journal = {Entropy},
  volume = {21},
  number = {10},
  pages = {1023},
  issn = {1099-4300},
  doi = {10.3390/e21101023},
  url = {https://www.mdpi.com/1099-4300/21/10/1023},
  urldate = {2021-07-05},
  abstract = {Ordinal patterns are the common basis of various techniques used in the study of dynamical systems and nonlinear time series analysis. The present article focusses on the computational problem of turning time series into sequences of ordinal patterns. In a first step, a numerical encoding scheme for ordinal patterns is proposed. Utilising the classical Lehmer code, it enumerates ordinal patterns by consecutive non-negative integers, starting from zero. This compact representation considerably simplifies working with ordinal patterns in the digital domain. Subsequently, three algorithms for the efficient extraction of ordinal patterns from time series are discussed, including previously published approaches that can be adapted to the Lehmer code. The respective strengths and weaknesses of those algorithms are discussed, and further substantiated by benchmark results. One of the algorithms stands out in terms of scalability: its run-time increases linearly with both the pattern order and the sequence length, while its memory footprint is practically negligible. These properties enable the study of high-dimensional pattern spaces at low computational cost. In summary, the tools described herein may improve the efficiency of virtually any ordinal pattern-based analysis method, among them quantitative measures like permutation entropy and symbolic transfer entropy, but also techniques like forbidden pattern identification. Moreover, the concepts presented may allow for putting ideas into practice that up to now had been hindered by computational burden. To enable smooth evaluation, a function library written in the C programming language, as well as language bindings and native implementations for various numerical computation environments are provided in the supplements.},
  langid = {english},
  annotation = {ZSCC: 0000006}
}

@incollection{beylinExtractingProofCoherence1996,
  title = {Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids},
  booktitle = {Types for {{Proofs}} and {{Programs}}},
  author = {Beylin, Ilya and Dybjer, Peter},
  editor = {Goos, Gerhard and Hartmanis, Juris and Leeuwen, Jan and Berardi, Stefano and Coppo, Mario},
  year = {1996},
  volume = {1158},
  pages = {47--61},
  publisher = {{Springer Berlin Heidelberg}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/3-540-61780-9_61},
  url = {http://link.springer.com/10.1007/3-540-61780-9_61},
  urldate = {2021-07-07},
  abstract = {This paper studies the problem of coherence in category theory from a type-theoretic viewpoint. We first show how a Curry-Howard interpretation of a formal proof of normalization for monoids almost directly yields a coherence proof for monoidal categories. Then we formalize this coherence proof in intensional intuitionistic type theory and show how it relies on explicit reasoning about proof objects for intensional equality. This formalization has been checkedin the proof assistant ALF.},
  isbn = {978-3-540-61780-8 978-3-540-70722-6},
  langid = {english}
}

@article{blackwellTwodimensionalMonadTheory1989,
  title = {Two-Dimensional Monad Theory},
  author = {Blackwell, R. and Kelly, G. M. and Power, A. J.},
  year = {1989},
  month = jul,
  journal = {Journal of Pure and Applied Algebra},
  volume = {59},
  number = {1},
  pages = {1--41},
  issn = {0022-4049},
  doi = {10.1016/0022-4049(89)90160-6},
  url = {10.1016/0022-4049(89)90160-6},
  urldate = {2021-06-12},
  abstract = {We consider a 2-monad T with rank on a complete and cocomplete 2-category, and write T-Alg for the 2-category given the T-algebras, the morphisms preserving the structure to within coherent isomorphisms, and the appropriate 2-cells; T-Algs is the sub-2-category obtained by taking the strict morphisms. We show that T-Alg admits pseudo-limits and certain other limits, and that the inclusion 2-functor T-Algs \textrightarrow{} T-Alg has a left adjoint. We introduce the notion of flexible algebra, and use it to prove that T-Alg admits all bicolimits and that the 2-functor T-Alg \textrightarrow{} S-Alg induced by a monad-map S \textrightarrow{} T admits a left biadjoint.},
  langid = {english},
  annotation = {ZSCC: 0000302}
}

@inproceedings{bowmanDaggerTracedSymmetric2011,
  title = {Dagger {{Traced Symmetric Monoidal Categories}} and {{Reversible Programming}}},
  booktitle = {Workshop on {{Reversible Computation}}},
  author = {Bowman, William J. and James, Roshan P. and Sabry, Amr},
  year = {2011},
  abstract = {We develop a reversible programming language from elementary mathematical and categorical foundations. The core language is based on isomorphisms between finite types: it is complete for combinational circuits and has an elegant semantics in dagger symmetric monoidal categories. The categorical semantics enables the definition of canonical and well-behaved reversible loop operators based on the notion of traced categories. The extended language can express recursive reversible algorithms on recursive types such as the natural numbers, lists, and trees. Computations in the extended language may diverge but every terminating computation is still reversible.}
}

@inproceedings{buchholtzHigherGroupsHomotopy2018,
  title = {Higher {{Groups}} in {{Homotopy Type Theory}}},
  booktitle = {Proceedings of the 33rd {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Buchholtz, Ulrik and {van Doorn}, Floris and Rijke, Egbert},
  year = {2018},
  month = jul,
  pages = {205--214},
  publisher = {{ACM}},
  address = {{Oxford United Kingdom}},
  doi = {10.1145/3209108.3209150},
  url = {https://dl.acm.org/doi/10.1145/3209108.3209150},
  urldate = {2021-06-16},
  abstract = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
  isbn = {978-1-4503-5583-4},
  langid = {english},
  annotation = {ZSCC: 0000018}
}

@inproceedings{buchholtzRealProjectiveSpaces2017,
  title = {The Real Projective Spaces in Homotopy Type Theory},
  booktitle = {Proceedings of the 32nd {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Buchholtz, Ulrik and Rijke, Egbert},
  year = {2017},
  month = jun,
  series = {{{LICS}} '17},
  pages = {1--8},
  publisher = {{IEEE Press}},
  address = {{Reykjav\'ik, Iceland}},
  abstract = {Homotopy type theory is a version of Martin-L\"of type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of RPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RPn by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP-1 to be the empty type. In the inductive step, we take RPn+1 to be the mapping cone of the projection map of the tautological bundle of RPn, and we use its universal property and the univalence axiom to define the tautological bundle on RPn+1. By showing that the total space of the tautological bundle of RPn is the n-sphere Sn, we retrieve the classical description of RPn+1 as RPn with an (n + 1)-disk attached to it. The infinite dimensional real projective space RP{$\infty$}, defined as the sequential colimit of RPn with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.},
  isbn = {978-1-5090-3018-7},
  keywords = {higher inductive types,homotopy type theory,real projective spaces,univalence axiom},
  annotation = {ZSCC: 0000014}
}

@incollection{caretteComputingSemiringsWeak2016,
  title = {Computing with {{Semirings}} and {{Weak Rig Groupoids}}},
  booktitle = {Programming {{Languages}} and {{Systems}}},
  author = {Carette, Jacques and Sabry, Amr},
  editor = {Thiemann, Peter},
  year = {2016},
  volume = {9632},
  pages = {123--148},
  publisher = {{Springer Berlin Heidelberg}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/978-3-662-49498-1_6},
  url = {http://link.springer.com/10.1007/978-3-662-49498-1_6},
  urldate = {2021-07-05},
  abstract = {The original formulation of the Curry\textendash Howard correspondence relates propositional logic to the simply-typed {$\lambda$}-calculus at three levels: the syntax of propositions corresponds to the syntax of types; the proofs of propositions correspond to programs of the corresponding types; and the normalization of proofs corresponds to the evaluation of programs. This rich correspondence has inspired our community for half a century and has been generalized to deal with more advanced logics and programming models. We propose a variant of this correspondence which is inspired by conservation of information and recent homotopy theoretic approaches to type theory.},
  isbn = {978-3-662-49497-4 978-3-662-49498-1},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{caretteEmbracingLawsPhysics2021,
  title = {Embracing the {{Laws}} of {{Physics}}: Three {{Reversible Models}} of {{Computation}}},
  shorttitle = {Embracing the {{Laws}} of {{Physics}}},
  author = {Carette, Jacques and James, Roshan P. and Sabry, Amr},
  year = {2021},
  journal = {Advances in Computers},
  volume = {126},
  url = {http://arxiv.org/abs/1811.03678},
  urldate = {2021-11-10},
  abstract = {Our main models of computation (the Turing Machine and the RAM) and most modern computer architectures make fundamental assumptions about which primitive operations are realizable on a physical computing device. The consensus is that these primitive operations include logical operations like conjunction, disjunction and negation, as well as reading and writing to a large collection of memory locations. This perspective conforms to a macro-level view of physics and indeed these operations are realizable using macro-level devices involving thousands of electrons. This point of view is however incompatible with computation realized using quantum devices or analyzed using elementary thermodynamics as both these fundamental physical theories imply that information is a conserved quantity of physical processes and hence of primitive computational operations.},
  langid = {english},
  keywords = {68Q05,Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Category Theory,Quantum Physics},
  annotation = {To appear}
}

@article{caretteReversibleProgramsUnivalent2018,
  title = {From {{Reversible Programs}} to {{Univalent Universes}} and {{Back}}},
  author = {Carette, Jacques and Chen, Chao-Hong and Choudhury, Vikraman and Sabry, Amr},
  year = {2018},
  month = apr,
  journal = {Electronic Notes in Theoretical Computer Science},
  series = {The {{Thirty}}-Third {{Conference}} on the {{Mathematical Foundations}} of {{Programming Semantics}} ({{MFPS XXXIII}})},
  volume = {336},
  pages = {5--25},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2018.03.013},
  url = {https://www.sciencedirect.com/science/article/pii/S1571066118300161},
  urldate = {2021-05-03},
  abstract = {We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simple computational interpretation of paths and of univalence in terms of familiar programming constructs whenever the universe in question is computable.},
  langid = {english},
  keywords = {Agda,Reversible programming,unilance},
  annotation = {ZSCC: 0000005}
}

@article{chenComputationalInterpretationCompact2021,
  title = {A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types},
  shorttitle = {A Computational Interpretation of Compact Closed Categories},
  author = {Chen, Chao-Hong and Sabry, Amr},
  year = {2021},
  month = jan,
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  pages = {9:1--9:29},
  doi = {10.1145/3434290},
  url = {https://doi.org/10.1145/3434290},
  urldate = {2021-07-02},
  abstract = {Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions. Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.},
  keywords = {Abstract Machines,Duality of Computation,Higher-Order Reversible Programming,Termination Proofs,Type Isomorphisms},
  annotation = {ZSCC: 0000001}
}

@inproceedings{chenFractionalTypes2020,
  title = {Fractional {{Types}}},
  booktitle = {Reversible {{Computation}}},
  author = {Chen, Chao-Hong and Choudhury, Vikraman and Carette, Jacques and Sabry, Amr},
  year = {2020},
  month = jul,
  pages = {169--186},
  publisher = {{Springer, Cham}},
  doi = {10.1007/978-3-030-52482-1_10},
  url = {https://link.springer.com/chapter/10.1007/978-3-030-52482-1_10},
  urldate = {2021-10-30},
  abstract = {In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching...},
  langid = {english}
}

@misc{choudhuryArtifactSymmetriesReversible2021,
  title = {Artifact for {{Symmetries}} in {{Reversible Programming}}},
  author = {Choudhury, Vikraman and Karwowski, Jacek and Sabry, Amr},
  year = {2021},
  month = oct,
  doi = {10.5281/zenodo.5671746},
  url = {https://zenodo.org/record/5671746},
  urldate = {2021-11-11},
  abstract = {Artifact for POPL'22},
  howpublished = {Zenodo}
}

@article{choudhuryFinitemultisetConstructionHoTT2019,
  title = {The Finite-Multiset Construction in {{HoTT}}},
  author = {Choudhury, Vikraman and Fiore, Marcelo},
  year = {2019},
  month = aug,
  pages = {40},
  url = {https://hott.github.io/HoTT-2019/conf-slides/Choudhury.pdf},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: NoCitationData[s1]}
}

@article{choudhuryFreeCommutativeMonoids2021,
  title = {Free {{Commutative Monoids}} in {{Homotopy Type Theory}}},
  author = {Choudhury, Vikraman and Fiore, Marcelo},
  year = {2021},
  month = oct,
  url = {https://arxiv.org/abs/2110.05412v1},
  urldate = {2021-10-27},
  abstract = {We develop a constructive theory of finite multisets, defining them as free commutative monoids in Homotopy Type Theory. We formalise two algebraic presentations of this construction using 1-HITs, establishing the universal property for each and thereby their equivalence. These presentations correspond to equational theories including a commutation axiom. In this setting, we prove important structural combinatorial properties of singleton multisets arising from concatenations and projections of multisets. This is done in generality, without assuming decidable equality on the carrier set. Further, as applications, we present a constructive formalisation of the relational model of differential linear logic and use it to characterise the equality type of multisets. This leads us to the introduction of a novel conditional equational presentation of the finite-multiset construction.},
  langid = {english}
}

@article{choudhurySymmetriesReversibleProgramming2021,
  title = {Symmetries in {{Reversible Programming}}: From {{Symmetric Rig Groupoids}} to {{Reversible Programming Languages}}},
  shorttitle = {Symmetries in {{Reversible Programming}}},
  author = {Choudhury, Vikraman and Karwowski, Jacek and Sabry, Amr},
  year = {2021},
  month = oct,
  url = {https://arxiv.org/abs/2110.05404v1},
  urldate = {2021-10-27},
  abstract = {The \$\textbackslash mathit\{\textbackslash Pi\}\$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids \textbackslash `a la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of reversible circuits. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, establishing full abstraction and adequacy. We extend the already established Curry-Howard correspondence for \$\textbackslash mathit\{\textbackslash Pi\}\$ to a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of \$\textbackslash mathit\{\textbackslash Pi\}\$ is presented by the free symmetric rig groupoid, given by finite sets and permutations. Our proof uses techniques from the theory of group presentations and rewriting systems to solve the word problem for symmetric groups. Using the formalisation of our results, we show how to perform normalisation-by-evaluation, verification, and synthesis of reversible logic gates, motivated by examples from quantum computing.},
  langid = {english}
}

@article{christensenCharacterizationUnivalentFibrations2015,
  title = {A {{Characterization}} of {{Univalent Fibrations}}},
  author = {Christensen, Dan},
  year = {2015},
  month = jun,
  pages = {53},
  url = {http://sweet.ua.pt/dirk/ct2015/slides/Christensen.pdf},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000002}
}

@article{cohenCoherenceRewriting2theories2009,
  title = {Coherence for Rewriting 2-Theories},
  author = {Cohen, Jonathan Asher},
  year = {2009},
  month = apr,
  journal = {arXiv:0904.0125 [cs, math]},
  eprint = {0904.0125},
  eprinttype = {arxiv},
  primaryclass = {cs, math},
  url = {http://arxiv.org/abs/0904.0125},
  urldate = {2021-06-28},
  abstract = {General coherence theorems are constructed that yield explicit presentations of categorical and algebraic objects. The categorical structures involved are finitary discrete Lawvere 2-theories, though they are approached within the language of term rewriting theory. Two general coherence theorems are obtained. The first applies to terminating and confluent rewriting 2-theories. This result is exploited to construct systematic presentations for the higher Thompson groups and the Higman-Thompson groups. The presentations are categorically interesting as they arise from higher-arity analogues of the Stasheff/Mac Lane coherence axioms, which involve phenomena not present in the classical binary axioms. The second general coherence theorem holds for 2-theories that are not necessarily confluent or terminating and is used to construct a new proof of coherence for iterated monoidal categories, which arise as categorical models of iterated loop spaces and fail to be confluent.},
  archiveprefix = {arXiv},
  keywords = {⛔ No DOI found,18C10,18D99,20F05,68Q42,Computer Science - Logic in Computer Science,Mathematics - Category Theory},
  annotation = {ZSCC: 0000002}
}

@article{cohenCubicalTypeTheory2018,
  title = {Cubical {{Type Theory}}: A {{Constructive Interpretation}} of the {{Univalence Axiom}}},
  shorttitle = {Cubical {{Type Theory}}},
  author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M{\"o}rtberg, Anders},
  year = {2018},
  pages = {34 pages},
  publisher = {{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany}},
  doi = {10.4230/LIPICS.TYPES.2015.5},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/8475/},
  urldate = {2021-06-29},
  abstract = {This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.},
  collaborator = {Herbstritt, Marc},
  langid = {english},
  keywords = {000 Computer science; knowledge; general works,Computer Science},
  annotation = {ZSCC: NoCitationData[s1]}
}

@book{curryCurryEssaysCombinatory1980,
  title = {To {{H}}.{{B}}. {{Curry}}: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
  shorttitle = {To {{H}}.{{B}}. {{Curry}}},
  editor = {Curry, Haskell B. and Hindley, J. Roger and Seldin, J. P.},
  year = {1980},
  publisher = {{Academic Press}},
  address = {{London ; New York}},
  isbn = {978-0-12-349050-6},
  lccn = {QA9.2 .T6},
  keywords = {Curry; Haskell B,Haskell Brooks,Logic; Symbolic and mathematical},
  annotation = {ZSCC: 0000016}
}

@inproceedings{danosReversibleCommunicatingSystems2004,
  title = {Reversible {{Communicating Systems}}},
  booktitle = {{{CONCUR}} 2004 - {{Concurrency Theory}}},
  author = {Danos, Vincent and Krivine, Jean},
  editor = {Gardner, Philippa and Yoshida, Nobuko},
  year = {2004},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {292--307},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/978-3-540-28644-8_19},
  abstract = {One obtains in this paper a process algebra RCCS, in the style of CCS, where processes can backtrack. Backtrack, just as plain forward computation, is seen as a synchronization and incurs no additional cost on the communication structure. It is shown that, given a past, a computation step can be taken back if and only if it leads to a causally equivalent past.},
  isbn = {978-3-540-28644-8},
  langid = {english},
  keywords = {Forward Action,Forward Transition,Monitor Process,Naming Scheme,Structural Congruence}
}

@book{davisGeometryTopologyCoxeter2008,
  title = {The Geometry and Topology of Coxeter Groups},
  author = {Davis, Michael},
  year = {2008},
  series = {London {{Mathematical Society}} Monographs Series},
  publisher = {{Princeton University Press}},
  address = {{Princeton}},
  isbn = {978-0-691-13138-2},
  langid = {english},
  lccn = {QA183 .D38 2008},
  keywords = {Coxeter groups,Geometric group theory},
  annotation = {ZSCC: NoCitationData[s1]  OCLC: ocm77485786}
}

@article{dipierroReversibleCombinatoryLogic2006,
  title = {Reversible Combinatory Logic},
  author = {Di Pierro, Alessandra and Hankin, Chris and Wiklicky, Herbert},
  year = {2006},
  month = aug,
  journal = {Mathematical Structures in Computer Science},
  volume = {16},
  number = {4},
  pages = {621--637},
  issn = {0960-1295},
  doi = {10.1017/S0960129506005391},
  url = {https://doi.org/10.1017/S0960129506005391},
  urldate = {2021-11-10},
  abstract = {The \$\textbackslash lambda\$-calculus is destructive: its main computational mechanism, beta reduction, destroys the redex, which makes replaying the computational steps impossible. Combinatory logic is a variant of the \$\textbackslash lambda\$-calculus that maintains irreversibility. Recently, reversible computational models have been studied mainly in the context of quantum computation, as (without measurements) quantum physics is inherently reversible. However, reversibility also fundamentally changes the semantical framework in which classical computation has to be investigated. We describe an implementation of classical combinatory logic in a reversible calculus for which we present an algebraic model based on a generalisation of the notion of a group.}
}

@article{duboisTestsProofsCustom2018,
  title = {Tests and Proofs for Custom Data Generators},
  author = {Dubois, Catherine and Giorgetti, Alain},
  year = {2018},
  month = nov,
  journal = {Formal Aspects of Computing},
  volume = {30},
  number = {6},
  pages = {659--684},
  issn = {0934-5043, 1433-299X},
  doi = {10.1007/s00165-018-0459-1},
  url = {http://link.springer.com/10.1007/s00165-018-0459-1},
  urldate = {2021-06-14},
  abstract = {We address automated testing and interactive proving of properties involving complex data structures with constraints, like the ones studied in enumerative combinatorics, e.g., permutations and maps. In this paper we show testing techniques to check properties of custom data generators for these structures. We focus on random property-based testing and bounded exhaustive testing, to find counterexamples for false conjectures in the Coq proof assistant. For random testing we rely on the existing Coq plugin QuickChick and its toolbox to write random generators. For bounded exhaustive testing, we use logic programming to generate all the data up to a given size. We also propose an extension of QuickChick with bounded exhaustive testing based on generators developed inside Coq, but also on correct-by-construction generators developed with Why3. These tools are applied to an original Coq formalization of the combinatorial structures of permutations and rooted maps, together with some operations on them and properties about them. Recursive generators are defined for each combinatorial family. They are used for debugging properties which are finally proved in Coq. This large case study is also a contribution in enumerative combinatorics.},
  langid = {english},
  annotation = {ZSCC: 0000004}
}

@article{elguetaGroupoidFiniteSets2021,
  title = {The Groupoid of Finite Sets Is Biinitial in the 2-Category of Rig Categories},
  author = {Elgueta, Josep},
  year = {2021},
  month = nov,
  journal = {Journal of Pure and Applied Algebra},
  volume = {225},
  number = {11},
  pages = {106738},
  issn = {0022-4049},
  doi = {10.1016/j.jpaa.2021.106738},
  url = {https://www.sciencedirect.com/science/article/pii/S0022404921000785},
  urldate = {2021-07-09},
  abstract = {The groupoid of finite sets has a ``canonical'' structure of a symmetric 2-rig with the sum and product respectively given by the coproduct and product of sets. This 2-rig FSet\textasciicircum{} is just one of the many non-equivalent categorifications of the commutative rig N of natural numbers, together with the rig N itself viewed as a discrete rig category, the whole category of finite sets, the category of finite dimensional vector spaces over a field k, etc. In this paper it is shown that FSet\textasciicircum{} is the right categorification of N in the sense that it is biinitial in the 2-category of rig categories, in the same way as N is initial in the category of rigs. As a by-product, an explicit description of the homomorphisms of rig categories from a suitable version of FSet\textasciicircum{} into any (semistrict) rig category S is obtained in terms of a sequence of automorphisms of the objects 1+{$\cdots$}n)+1 in S for each n{$\geq$}0.},
  langid = {english},
  keywords = {Categorification,Groupoid of finite sets,Rig categories},
  annotation = {ZSCC: 0000001}
}

@article{feynmanSimulatingPhysicsComputers1982,
  title = {Simulating Physics with Computers},
  author = {Feynman, Richard P.},
  year = {1982},
  month = jun,
  journal = {International Journal of Theoretical Physics},
  volume = {21},
  number = {6},
  pages = {467--488},
  issn = {1572-9575},
  doi = {10.1007/BF02650179},
  url = {https://doi.org/10.1007/BF02650179},
  urldate = {2021-11-10},
  langid = {english}
}

@article{fioreCartesianClosedBicategory2008,
  title = {The Cartesian Closed Bicategory of Generalised Species of Structures},
  author = {Fiore, M. and Gambino, N. and Hyland, M. and Winskel, G.},
  year = {2008},
  month = feb,
  journal = {Journal of the London Mathematical Society},
  volume = {77},
  number = {1},
  pages = {203--220},
  issn = {00246107},
  doi = {10.1112/jlms/jdm096},
  url = {http://doi.wiley.com/10.1112/jlms/jdm096},
  urldate = {2021-06-29},
  abstract = {The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These definitions encompass most notions of combinatorial species considered in the literature\textemdash including of course Joyal's original notion\textemdash together with their associated substitution operation. Our first main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.},
  langid = {english},
  annotation = {ZSCC: 0000087}
}

@inproceedings{fioreIsomorphismsGenericRecursive2004,
  title = {Isomorphisms of Generic Recursive Polynomial Types},
  booktitle = {Proceedings of the 31st {{ACM SIGPLAN}}-{{SIGACT}} Symposium on {{Principles}} of Programming Languages},
  author = {Fiore, Marcelo},
  year = {2004},
  month = jan,
  series = {{{POPL}} '04},
  pages = {77--88},
  publisher = {{Association for Computing Machinery}},
  address = {{New York, NY, USA}},
  doi = {10.1145/964001.964008},
  url = {https://doi.org/10.1145/964001.964008},
  urldate = {2021-06-11},
  abstract = {This paper gives the first decidability results on type isomorphism for recursive types, establishing the explicit decidability of type isomorphism for the type theory of sums and products over an inhabited generic recursive polynomial type. The technical development provides connections between themes in programming-language theory (type isomorphism) and computational algebra (Gr\"obner bases).},
  isbn = {978-1-58113-729-3},
  keywords = {data structure,Gröbner bases,recursive types,rigs,semigroups,type isomorphism,type theory,word problem},
  annotation = {ZSCC: 0000040}
}

@inproceedings{fioreRemarksIsomorphismsTyped2002,
  title = {Remarks on {{Isomorphisms}} in {{Typed Lambda Calculi}} with {{Empty}} and {{Sum Types}}},
  booktitle = {Proceedings of the 17th {{Annual IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Fiore, Marcelo P. and Cosmo, Roberto Di and Balat, Vincent},
  year = {2002},
  month = jul,
  series = {{{LICS}} '02},
  pages = {147},
  publisher = {{IEEE Computer Society}},
  address = {{USA}},
  abstract = {Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed lambda calculus, where the constant for one and the operations of product and exponentiation respectively correspond to the unit type and the product and arrow type constructors. This paper studies isomorphisms in typed lambda calculiwith empty and sum types from this viewpoint. We close an open problem by establishing that the theory of type isomorphisms in the presence of product, arrow, and sum types (with or without the unit type) is not finitely axiomatisable. Further, we observe that for type theories with arrow, empty and sum types the correspondence between isomorphism and arithmetic equality generally breaks down, but that it still holds in some particular cases including that of type isomorphism with the empty type and equality with zero.},
  isbn = {978-0-7695-1483-3},
  annotation = {ZSCC: 0000023}
}

@inproceedings{fioreSecondOrderAlgebraicTheories2010,
  title = {Second-{{Order Algebraic Theories}}},
  booktitle = {Mathematical {{Foundations}} of {{Computer Science}} 2010},
  author = {Fiore, Marcelo and Mahmoud, Ola},
  editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'i}n},
  year = {2010},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {368--380},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/978-3-642-15155-2_33},
  url = {10.1007/978-3-642-15155-2_33},
  abstract = {Fiore and Hur [10] recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a formal deductive system for languages with variable binding and parameterised metavariables. This work completes the foundations of the subject from the viewpoint of categorical algebra. Specifically, the paper introduces the notion of second-order algebraic theory and develops its basic theory. Two categorical equivalences are established: at the syntactic level, that of second-order equational presentations and second-order algebraic theories; at the semantic level, that of second-order algebras and second-order functorial models. Our development includes a mathematical definition of syntactic translation between second-order equational presentations. This gives the first formalisation of notions such as encodings and transforms in the context of languages with variable binding.},
  isbn = {978-3-642-15155-2},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s1]}
}

@article{forestCoherenceGrayCategories2018,
  title = {Coherence of {{Gray Categories}} via {{Rewriting}}},
  author = {Forest, Simon and Mimram, Samuel},
  year = {2018},
  pages = {16 pages},
  publisher = {{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany}},
  doi = {10.4230/LIPICS.FSCD.2018.15},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/9185/},
  urldate = {2021-07-09},
  abstract = {Over the recent years, the theory of rewriting has been extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to low-dimensional weak categories, and consider in details the first non-trivial case: presentations of tricategories. By a general result, those are equivalent to the stricter Gray categories, for which we introduce a notion of rewriting system, as well as associated tools: critical pairs, termination orders, etc. We show that a finite rewriting system admits a finite number of critical pairs and, as a variant of Newman's lemma in our context, that a convergent rewriting system is coherent, meaning that two parallel 3-cells are necessarily equal. This is illustrated on rewriting systems corresponding to various well-known structures in the context of Gray categories (monoids, adjunctions, Frobenius monoids). Finally, we discuss generalizations in arbitrary dimension.},
  collaborator = {Wagner, Michael},
  langid = {english},
  keywords = {000 Computer science; knowledge; general works,Computer Science},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{forestCoherenceGrayCategories2018a,
  title = {Coherence of {{Gray Categories}} via {{Rewriting}}},
  author = {Forest, Simon and Mimram, Samuel},
  year = {2018},
  pages = {16 pages},
  publisher = {{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany}},
  doi = {10.4230/LIPICS.FSCD.2018.15},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/9185/},
  urldate = {2021-07-09},
  abstract = {Over the recent years, the theory of rewriting has been extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to low-dimensional weak categories, and consider in details the first non-trivial case: presentations of tricategories. By a general result, those are equivalent to the stricter Gray categories, for which we introduce a notion of rewriting system, as well as associated tools: critical pairs, termination orders, etc. We show that a finite rewriting system admits a finite number of critical pairs and, as a variant of Newman's lemma in our context, that a convergent rewriting system is coherent, meaning that two parallel 3-cells are necessarily equal. This is illustrated on rewriting systems corresponding to various well-known structures in the context of Gray categories (monoids, adjunctions, Frobenius monoids). Finally, we discuss generalizations in arbitrary dimension.},
  collaborator = {Wagner, Michael},
  langid = {english},
  keywords = {000 Computer science; knowledge; general works,Computer Science}
}

@phdthesis{frankReversibilityEfficientComputing1999,
  title = {Reversibility for Efficient Computing},
  author = {Frank, Michael P.},
  year = {1999},
  address = {{USA}},
  abstract = {Today's computers are based on irreversible logic devices, which have been known to be fundamentally energy-inefficient for several decades. Recently, alternative reversible logic technologies have improved rapidly, and are now becoming practical. In traditional models of computation, pure reversibility seems to decrease overall computational efficiency; I provide a proof to this effect. However, traditional models ignore important physical constraints on information processing. This thesis gives the first analysis demonstrating that in a realistic model of computation that accounts for thermodynamic issues, as well as other physical constraints, the judicious use of reversible computing can strictly increase asymptotic computational efficiency, as machine sizes increase. I project real benefits for supercomputing at a large (but achievable) scale in the fairly near term. And with proposed future computing technologies, I show that reversibility will benefit computing at all scales. Next, the thesis demonstrates that reversible computing techniques do not make computer design much more difficult. I describe how to design asymptotically efficient processors using an ``adiabatic'' reversible electronic logic technology that can be built with today's microprocessor fabrication processes. I describe a simple universal reversible parallel processor chip that our group recently fabricated, and a reversible instruction set for a more traditional RISC-style uniprocessor. Finally, I describe techniques for programming reversible computers. I present a high-level language and a compiler suitable for coding efficient reversible algorithms, and I describe a variety of example algorithms, including efficient reversible sorting, searching, arithmetic, matrix, and graph algorithms. As an example application, I present a linear-time, constant-space reversible program for simulating the Schr\"odinger wave equation of quantum mechanics. (Copies available exclusively from MIT Libraries, Rm. 14-0551, Cambridge, MA 02139-4307. Ph. 617-253-5668; Fax 617-253-1690.)},
  school = {Massachusetts Institute of Technology},
  annotation = {AAI0800784}
}

@article{fredkinConservativeLogic1982,
  title = {Conservative Logic},
  author = {Fredkin, Edward and Toffoli, Tommaso},
  year = {1982},
  month = apr,
  journal = {International Journal of Theoretical Physics},
  volume = {21},
  number = {3},
  pages = {219--253},
  issn = {1572-9575},
  doi = {10.1007/BF01857727},
  url = {https://doi.org/10.1007/BF01857727},
  urldate = {2021-11-10},
  abstract = {Conservative logic is a comprehensive model of computation which explicitly reflects a number of fundamental principles of physics, such as the reversibility of the dynamical laws and the conservation of certainadditive quantities (among which energy plays a distinguished role). Because it more closely mirrors physics than traditional models of computation, conservative logic is in a better position to provide indications concerning the realization of high-performance computing systems, i.e., of systems that make very efficient use of the ``computing resources'' actually offered by nature. In particular, conservative logic shows that it is ideally possible to build sequential circuits with zero internal power dissipation. After establishing a general framework, we discuss two specific models of computation. The first uses binary variables and is the conservative-logic counterpart of switching theory; this model proves that universal computing capabilities are compatible with the reversibility and conservation constraints. The second model, which is a refinement of the first, constitutes a substantial breakthrough in establishing a correspondence between computation and physics. In fact, this model is based on elastic collisions of identical ``balls,'' and thus is formally identical with the atomic model that underlies the (classical) kinetic theory of perfect gases. Quite literally, the functional behavior of a general-purpose digital computer can be reproduced by a perfect gas placed in a suitably shaped container and given appropriate initial conditions.},
  langid = {english}
}

@article{gurskiInfiniteLoopSpaces2013,
  title = {Infinite Loop Spaces, and Coherence for Symmetric Monoidal Bicategories},
  author = {Gurski, Nick and Osorno, Ang{\'e}lica M.},
  year = {2013},
  month = oct,
  journal = {Advances in Mathematics},
  volume = {246},
  pages = {1--32},
  issn = {0001-8708},
  doi = {10.1016/j.aim.2013.06.028},
  url = {https://www.sciencedirect.com/science/article/pii/S0001870813002387},
  urldate = {2021-07-09},
  abstract = {This paper proves three different coherence theorems for symmetric monoidal bicategories. First, we show that in a free symmetric monoidal bicategory every diagram of 2-cells commutes. Second, we show that this implies that the free symmetric monoidal bicategory on one object is equivalent, as a symmetric monoidal bicategory, to the discrete symmetric monoidal bicategory given by the disjoint union of the symmetric groups. Third, we show that every symmetric monoidal bicategory is equivalent to a strict one. We give two topological applications of these coherence results. First, we show that the classifying space of a symmetric monoidal bicategory can be equipped with an E{$\infty$} structure. Second, we show that the fundamental 2-groupoid of an En space, n{$\geq$}4, has a symmetric monoidal structure. These calculations also show that the fundamental 2-groupoid of an E3 space has a sylleptic monoidal structure.},
  langid = {english},
  keywords = {Coherence,space,Symmetric monoidal bicategory},
  annotation = {ZSCC: 0000026}
}

@article{gylterudMultisetsTypeTheory2020,
  title = {Multisets in Type Theory},
  author = {Gylterud, H{\aa}kon Robbestad},
  year = {2020},
  month = jul,
  journal = {Mathematical Proceedings of the Cambridge Philosophical Society},
  volume = {169},
  number = {1},
  pages = {1--18},
  publisher = {{Cambridge University Press}},
  issn = {0305-0041, 1469-8064},
  doi = {10.1017/S0305004119000045},
  url = {https://www.cambridge.org/core/journals/mathematical-proceedings-of-the-cambridge-philosophical-society/article/abs/multisets-in-type-theory/C17604B9927E477B70126529A2A91321#access-block},
  urldate = {2021-07-07},
  abstract = {A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin\textendash L\"of Type Theory, in the presence of Voevodsky's Univalence Axiom.In his 1978 paper, ``the type theoretic interpretation of constructive set theory'' Aczel introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the univalence axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.},
  langid = {english},
  keywords = {03B15},
  annotation = {ZSCC: 0000004}
}

@book{heyFeynmanComputationExploring1999,
  title = {Feynman and Computation: Exploring the Limits of Computers},
  shorttitle = {Feynman and Computation},
  editor = {Hey, Anthony J. G.},
  year = {1999},
  publisher = {{Perseus Books}},
  address = {{USA}},
  isbn = {978-0-7382-0057-6}
}

@misc{hiverCoqCombiCoxeterPresentation2021,
  title = {Coq-{{Combi}}: The {{Coxeter Presentation}} of the {{Symmetric Group}}},
  author = {Hiver, Florent},
  year = {2021},
  month = oct,
  url = {https://github.com/math-comp/Coq-Combi/blob/1ba924ecc1a1c7714a9b3a2dbb23d91af2a1193a/theories/SymGroup/presentSn.v},
  urldate = {2021-11-10},
  abstract = {Algebraic Combinatorics in Coq},
  copyright = {GPL-3.0},
  howpublished = {Mathematical Components},
  annotation = {Based on unfinished notes 'The Symmetric Group', by Alain Lascoux}
}

@article{huelsbergenLogicallyReversibleEvaluator1996,
  title = {A {{Logically Reversible Evaluator}} for the {{Call}}-by-Name {{Lambda Calculus}}},
  author = {Huelsbergen, Lorenz},
  year = {1996},
  journal = {InterJournal Complex Systems},
  volume = {46}
}

@article{huetConfluentReductionsAbstract1980,
  title = {Confluent {{Reductions}}: Abstract {{Properties}} and {{Applications}} to {{Term Rewriting Systems}}: Abstract {{Properties}} and {{Applications}} to {{Term Rewriting Systems}}},
  shorttitle = {Confluent {{Reductions}}},
  author = {Huet, G{\'e}rard},
  year = {1980},
  month = oct,
  journal = {Journal of the ACM},
  volume = {27},
  number = {4},
  pages = {797--821},
  issn = {0004-5411},
  doi = {10.1145/322217.322230},
  url = {10.1145/322217.322230},
  urldate = {2021-07-02},
  annotation = {ZSCC: 0001631}
}

@article{hylandClassicalLambdaCalculus2017,
  title = {Classical Lambda Calculus in Modern Dress},
  author = {Hyland, J. M. E.},
  year = {2017},
  month = jun,
  journal = {Mathematical Structures in Computer Science},
  volume = {27},
  number = {5},
  pages = {762--781},
  publisher = {{Cambridge University Press}},
  issn = {0960-1295, 1469-8072},
  doi = {10.1017/S0960129515000377},
  url = {10.1017/S0960129515000377},
  urldate = {2021-06-27},
  abstract = {Recent developments in the categorical foundations of universal algebra have given an impetus to an understanding of the lambda calculus coming from categorical logic: an interpretation is a semi-closed algebraic theory. Scott's representation theorem is then completely natural and leads to a precise Fundamental Theorem showing the essential equivalence between the categorical and more familiar notions.},
  langid = {english},
  annotation = {ZSCC: 0000026}
}

@article{hylandSymmetricMonoidalSketches2004,
  title = {Symmetric {{Monoidal Sketches}} and {{Categories}} of {{Wirings}}},
  author = {Hyland, Martin and Power, John},
  year = {2004},
  month = oct,
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {100},
  pages = {31--46},
  issn = {15710661},
  doi = {10.1016/j.entcs.2004.09.004},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S1571066104050984},
  urldate = {2021-06-29},
  abstract = {We introduce a potential application of two-dimensional linear algebra to concurrency. Motivated by the structure of categories of wirings, in particular in action calculi but also in other models of concurrency, we investigate the notion of symmetric monoidal sketch for providing an abstract notion of category of wirings. Every symmetric monoidal sketch generates a generic model. If the sketch is single-sorted, the generic model can be characterised as a free structure on 1, with structure defined coalgebraically. We investigate how these results generalise results about categories of wirings given by Milner and others, and we outline how the constructs may be extended to model controls and dynamics.},
  langid = {english},
  annotation = {ZSCC: 0000004}
}

@inproceedings{jamesInformationEffects2012,
  title = {Information Effects},
  booktitle = {Proceedings of the 39th Annual {{ACM SIGPLAN}}-{{SIGACT}} Symposium on {{Principles}} of Programming Languages},
  author = {James, Roshan P. and Sabry, Amr},
  year = {2012},
  month = jan,
  series = {{{POPL}} '12},
  pages = {73--84},
  publisher = {{Association for Computing Machinery}},
  address = {{New York, NY, USA}},
  doi = {10.1145/2103656.2103667},
  url = {https://doi.org/10.1145/2103656.2103667},
  urldate = {2021-06-14},
  abstract = {Computation is a physical process which, like all other physical processes, is fundamentally reversible. From the notion of type isomorphisms, we derive a typed, universal, and reversible computational model in which information is treated as a linear resource that can neither be duplicated nor erased. We use this model as a semantic foundation for computation and show that the "gap" between conventional irreversible computation and logically reversible computation can be captured by a type-and-effect system. Our type-and-effect system is structured as an arrow metalanguage that exposes creation and erasure of information as explicit effect operations. Irreversible computations arise from interactions with an implicit information environment, thus making them a derived notion, much like open systems in Physics. We sketch several applications which can benefit from an explicit treatment of information effects, such as quantitative information-flow security and differential privacy.},
  isbn = {978-1-4503-1083-3},
  keywords = {arrows,linear logic,quantum computing,reversible logic},
  annotation = {ZSCC: 0000048}
}

@inproceedings{jamesTheseusHighLevelLanguage2014,
  title = {Theseus: A {{High}}-{{Level Language}} for {{Reversible Computation}}},
  booktitle = {Reversible {{Computation}}},
  author = {James, Roshan P. and Sabry, Amr},
  year = {2014},
  annotation = {Booklet of work-in-progress and short reports}
}

@article{joyalBraidedTensorCategories1993,
  title = {Braided {{Tensor Categories}}},
  author = {Joyal, A. and Street, R.},
  year = {1993},
  month = nov,
  journal = {Advances in Mathematics},
  volume = {102},
  number = {1},
  pages = {20--78},
  issn = {0001-8708},
  doi = {10.1006/aima.1993.1055},
  url = {10.1006/aima.1993.1055},
  urldate = {2021-07-09},
  langid = {english},
  annotation = {ZSCC: 0001124}
}

@article{kapulkinSimplicialModelUnivalent2021,
  title = {The Simplicial Model of {{Univalent Foundations}} (after {{Voevodsky}})},
  author = {Kapulkin, Krzysztof and Lumsdaine, Peter LeFanu},
  year = {2021},
  month = mar,
  journal = {Journal of the European Mathematical Society},
  volume = {23},
  number = {6},
  pages = {2071--2126},
  issn = {1435-9855},
  doi = {10.4171/JEMS/1050},
  url = {10.4171/JEMS/1050},
  urldate = {2021-07-06},
  langid = {english},
  annotation = {ZSCC: 0000003}
}

@article{kapulkinUnivalenceSimplicialSets2012,
  title = {Univalence in {{Simplicial Sets}}},
  author = {Kapulkin, Chris and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir},
  year = {2012},
  month = mar,
  url = {https://arxiv.org/abs/1203.2553v1},
  urldate = {2021-10-27},
  abstract = {We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.},
  langid = {english}
}

@article{kapulkinUnivalenceSimplicialSets2018,
  title = {Univalence in {{Simplicial Sets}}},
  author = {Kapulkin, Chris and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir},
  year = {2018},
  month = oct,
  journal = {arXiv:1203.2553 [math]},
  eprint = {1203.2553},
  eprinttype = {arxiv},
  primaryclass = {math},
  url = {http://arxiv.org/abs/1203.2553},
  urldate = {2021-07-06},
  abstract = {We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.},
  archiveprefix = {arXiv},
  keywords = {⛔ No DOI found,55U10 (Primary) 55U35 (Secondary),Mathematics - Algebraic Topology,Mathematics - Category Theory},
  annotation = {ZSCC: NoCitationData[s0]}
}

@inproceedings{kellyCoherenceTheoremsLax1974,
  title = {Coherence Theorems for Lax Algebras and for Distributive Laws},
  booktitle = {Category {{Seminar}}},
  author = {Kelly, G. M.},
  editor = {Kelly, Gregory M.},
  year = {1974},
  series = {Lecture {{Notes}} in {{Mathematics}}},
  pages = {281--375},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/BFb0063106},
  isbn = {978-3-540-37270-7},
  langid = {english},
  keywords = {Closed Category,Monoidal Category,Natural Transformation,Symmetric Monoidal Category,Symmetric Monoidal Structure}
}

@inproceedings{klugeReversibleSECD2000,
  title = {A {{Reversible SE}}({{M}}){{CD Machine}}},
  booktitle = {Implementation of {{Functional Languages}}},
  author = {Kluge, Werner},
  editor = {Koopman, Pieter and Clack, Chris},
  year = {2000},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {95--113},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/10722298_6},
  abstract = {The paper describes the basic concept of a reversible functional computing machine which can reduce a program term to its (weak) normal form and then do inverse reductions which re-construct the initial program term. The machine under consideration is a variant of Landin's secd-machine which can evaluate terms of a simple applied {$\lambda$}-calculus both applicative and normal order. It includes some auxiliary run-time structures to accommodate the environment necessary for reverse computations. The machine is specified in terms of the state transition rules for both forward and backward computations.},
  isbn = {978-3-540-44658-3},
  langid = {english},
  keywords = {Normal Order,Program Term,Reverse Computation,Rule Application,Rule Index}
}

@book{knuthArtComputerProgramming1997,
  title = {The Art of Computer Programming},
  author = {Knuth, Donald Ervin},
  year = {1997},
  edition = {3rd ed},
  publisher = {{Addison-Wesley}},
  address = {{Reading, Mass}},
  isbn = {978-0-201-89683-1 978-0-201-89684-8 978-0-201-89685-5},
  lccn = {QA76.6 .K64 1997},
  keywords = {Computer algorithms,Computer programming},
  annotation = {ZSCC: 0025917}
}

@incollection{knuthSimpleWordProblems1970,
  title = {Simple {{Word Problems}} in {{Universal Algebras}}\textdagger\textdagger{{The}} Work Reported in This Paper Was Supported in Part by the {{U}}.{{S}}. {{Office}} of {{Naval Research}}.},
  booktitle = {Computational {{Problems}} in {{Abstract Algebra}}},
  author = {Knuth, DONALD E. and Bendix, PETER B.},
  editor = {Leech, JOHN},
  year = {1970},
  month = jan,
  pages = {263--297},
  publisher = {{Pergamon}},
  doi = {10.1016/B978-0-08-012975-4.50028-X},
  url = {https://www.sciencedirect.com/science/article/pii/B978008012975450028X},
  urldate = {2021-07-01},
  abstract = {An algorithm is described which is capable of solving certain word problems: i.e. of deciding whether or not two words composed of variables and operators can be proved equal as a consequence of a given set of identities satisfied by the operators. Although the general word problem is well known to be unsolvable, this algorithm provides results in many interesting cases. For example in elementary group theory if we are given the binary operator {$\cdot$}, the unary operator -, and the nullary operator e, the algorithm is capable of deducing from the three identities a {$\cdot$} (b {$\cdot$} c) = (a {$\cdot$} b) {$\cdot$} c, a {$\cdot$} a- = e, a {$\cdot$} e = a, the laws a- {$\cdot$} a = e, e {$\cdot$} a = a, a\textendash{} = a, etc.; and furthermore it can show that a {$\cdot$} b = b {$\cdot$} a- is not a consequence of the given axioms. The method is based on a well-ordering of the set of all words, such that each identity can be construed as a ``reduction'', in the sense that the right-hand side of the identity represents a word smaller in the ordering than the left-hand side. A set of reduction identities is said to be ``complete'' when two words are equal as a consequence of the identities if and only if they reduce to the same word by a series of reductions. The method used in this algorithm is essentially to test whether a given set of identities is complete; if it is not complete the algorithm in many cases finds a new consequence of the identities which can be added to the list. The process is repeated until either a complete set is achieved or until an anomalous situation occurs which cannot at present be handled. Results of several computational experiments using the algorithm are given.},
  isbn = {978-0-08-012975-4},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s0]}
}

@inproceedings{krausCoherenceWellFoundednessTaming2020,
  title = {Coherence via {{Well}}-{{Foundedness}}: Taming {{Set}}-{{Quotients}} in {{Homotopy Type Theory}}},
  shorttitle = {Coherence via {{Well}}-{{Foundedness}}},
  booktitle = {Proceedings of the 35th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Kraus, Nicolai and {von Raumer}, Jakob},
  year = {2020},
  month = jul,
  pages = {662--675},
  publisher = {{ACM}},
  address = {{Saarbr\"ucken Germany}},
  doi = {10.1145/3373718.3394800},
  url = {https://dl.acm.org/doi/10.1145/3373718.3394800},
  urldate = {2021-06-13},
  abstract = {Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of induction for cycles for the case that the graph is given as the symmetric closure of a locally confluent and (co-)wellfounded relation. We show that, assuming the property in question is sufficiently nice, it is enough to prove it for the empty cycle and for cycles given by local confluence.},
  isbn = {978-1-4503-7104-9},
  langid = {english},
  annotation = {ZSCC: 0000002}
}

@inproceedings{krausFreeHigherGroups2018,
  title = {Free {{Higher Groups}} in {{Homotopy Type Theory}}},
  booktitle = {Proceedings of the 33rd {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Kraus, Nicolai and Altenkirch, Thorsten},
  year = {2018},
  month = jul,
  pages = {599--608},
  publisher = {{ACM}},
  address = {{Oxford United Kingdom}},
  doi = {10.1145/3209108.3209183},
  url = {https://dl.acm.org/doi/10.1145/3209108.3209183},
  urldate = {2021-06-16},
  abstract = {Given a type A in homotopy type theory (HoTT), we can define the free {$\infty$}-group on A as the loop space of the suspension of A+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A), cons : A \textrightarrow{} F(A) \textrightarrow{} F(A), and conditions saying that every cons(a) is an auto-equivalence on F(A). Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether F(A) is a set as well, which is very much related to an open problem in the HoTT book [22, Ex. 8.2]. We show an approximation to the question, namely that the fundamental groups of F(A) are trivial, i.e. that {$\parallel$}F(A){$\parallel$}1 is a set.},
  isbn = {978-1-4503-5583-4},
  langid = {english},
  annotation = {ZSCC: 0000011}
}

@inproceedings{krogmeierDecidableSynthesisPrograms2020,
  title = {Decidable {{Synthesis}} of {{Programs}} with {{Uninterpreted Functions}}},
  booktitle = {Computer {{Aided Verification}}},
  author = {Krogmeier, Paul and Mathur, Umang and Murali, Adithya and Madhusudan, P. and Viswanathan, Mahesh},
  editor = {Lahiri, Shuvendu K. and Wang, Chao},
  year = {2020},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {634--657},
  publisher = {{Springer International Publishing}},
  address = {{Cham}},
  doi = {10.1007/978-3-030-53291-8_32},
  abstract = {We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs, and we show the problem to be decidable, identify its precise complexity, and also study several variants of the problem.},
  isbn = {978-3-030-53291-8},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{lafontAlgebraicTheoryBoolean2003,
  title = {Towards an Algebraic Theory of {{Boolean}} Circuits},
  author = {Lafont, Yves},
  year = {2003},
  month = nov,
  journal = {Journal of Pure and Applied Algebra},
  volume = {184},
  number = {2},
  pages = {257--310},
  issn = {0022-4049},
  doi = {10.1016/S0022-4049(03)00069-0},
  url = {https://www.sciencedirect.com/science/article/pii/S0022404903000690},
  urldate = {2021-11-10},
  abstract = {Boolean circuits are used to represent programs on finite data. Reversible Boolean circuits and quantum Boolean circuits have been introduced to modelize some physical aspects of computation. Those notions are essential in complexity theory, but we claim that a deep mathematical theory is needed to make progress in this area. For that purpose, the recent developments of knot theory is a major source of inspiration. Following the ideas of Burroni, we consider logical gates as generators for some algebraic structure with two compositions, and we are interested in the relations satisfied by those generators. For that purpose, we introduce canonical forms and rewriting systems. Up to now, we have mainly studied the basic case and the linear case, but we hope that our methods can be used to get presentations by generators and relations for the (reversible) classical case and for the (unitary) quantum case.},
  langid = {english}
}

@article{laisantNumerationFactorielleApplication1888,
  title = {{Sur la num\'eration factorielle, application aux permutations}},
  author = {Laisant, C.- A.},
  year = {1888},
  journal = {Bulletin de la Soci\'et\'e Math\'ematique de France},
  volume = {2},
  pages = {176--183},
  issn = {0037-9484, 2102-622X},
  doi = {10.24033/bsmf.378},
  url = {http://www.numdam.org/item?id=BSMF_1888__16__176_0},
  urldate = {2021-07-08},
  langid = {french},
  annotation = {ZSCC: 0000057}
}

@book{lambekIntroductionHigherOrder1994,
  title = {Introduction to Higher Order Categorical Logic},
  author = {Lambek, Joachim and Scott, Philip J. and Scott, P. J.},
  year = {1994},
  series = {Cambridge Studies in Advanced Mathematics},
  edition = {Paperback ed. (with corr.), reprinted},
  number = {7},
  publisher = {{Cambridge Univ. Press}},
  address = {{Cambridge}},
  isbn = {978-0-521-35653-4},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s1]}
}

@article{landauerIrreversibilityHeatGeneration1961,
  title = {Irreversibility and {{Heat Generation}} in the {{Computing Process}}},
  author = {Landauer, R.},
  year = {1961},
  month = jul,
  journal = {IBM Journal of Research and Development},
  volume = {5},
  number = {3},
  pages = {183--191},
  issn = {0018-8646},
  doi = {10.1147/rd.53.0183},
  abstract = {It is argued that computing machines inevitably involve devices which perform logical functions that do not have a single-valued inverse. This logical irreversibility is associated with physical irreversibility and requires a minimal heat generation, per machine cycle, typically of the order of kT for each irreversible function. This dissipation serves the purpose of standardizing signals and making them independent of their exact logical history. Two simple, but representative, models of bistable devices are subjected to a more detailed analysis of switching kinetics to yield the relationship between speed and energy dissipation, and to estimate the effects of errors induced by thermal fluctuations.}
}

@inproceedings{laplazaCoherenceDistributivity1972,
  title = {Coherence for Distributivity},
  booktitle = {Coherence in {{Categories}}},
  author = {Laplaza, Miguel L.},
  editor = {Kelly, G. M. and Laplaza, M. and Lewis, G. and Mac Lane, Saunders},
  year = {1972},
  series = {Lecture {{Notes}} in {{Mathematics}}},
  pages = {29--65},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/BFb0059555},
  isbn = {978-3-540-37958-4},
  langid = {english},
  keywords = {Analogous Case,Coherence Condition,Commutative Diagram,Natural Morphism,Regular Element}
}

@article{lawvereFUNCTORIALSEMANTICSALGEBRAIC1963,
  title = {{{FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES}}},
  author = {Lawvere, F. William},
  year = {1963},
  month = nov,
  journal = {Proceedings of the National Academy of Sciences},
  volume = {50},
  number = {5},
  pages = {869--872},
  doi = {10.1073/pnas.50.5.869},
  url = {10.1073/pnas.50.5.869},
  annotation = {ZSCC: 0001425}
}

@incollection{lehmerTeachingCombinatorialTricks1960,
  title = {Teaching Combinatorial Tricks to a Computer},
  booktitle = {Proceedings of {{Symposia}} in {{Applied Mathematics}}},
  author = {Lehmer, D. H.},
  editor = {Bellman, Richard and Hall, Marshall},
  year = {1960},
  volume = {10},
  pages = {179--193},
  publisher = {{American Mathematical Society}},
  address = {{Providence, Rhode Island}},
  doi = {10.1090/psapm/010/0113289},
  url = {https://doi.org/10.1090/psapm/010},
  urldate = {2021-01-30},
  isbn = {978-0-8218-1310-2 978-0-8218-9225-1},
  langid = {english},
  annotation = {ZSCC: NoCitationData[s2]}
}

@book{leinsterHigherOperadsHigher2004,
  title = {Higher {{Operads}}, {{Higher Categories}}},
  author = {Leinster, Tom},
  year = {2004},
  series = {London {{Mathematical Society Lecture Note Series}}},
  publisher = {{Cambridge University Press}},
  address = {{Cambridge}},
  doi = {10.1017/CBO9780511525896},
  url = {https://www.cambridge.org/core/books/higher-operads-higher-categories/E4BC6645A0DA99C2A9D50D8993BA54A9},
  urldate = {2021-06-12},
  abstract = {Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. This is the first book on the subject and lays its foundations. It will appeal to both graduate students and established researchers who wish to become acquainted with this modern branch of mathematics.},
  isbn = {978-0-521-53215-0},
  annotation = {ZSCC: 0000876}
}

@article{maclaneNaturalAssociativityCommutativity1963,
  title = {Natural {{Associativity}} and {{Commutativity}}},
  author = {MacLane, Saunders},
  year = {1963},
  month = oct,
  journal = {Rice Institute Pamphlet - Rice University Studies},
  volume = {49},
  number = {4},
  publisher = {{Rice University}},
  url = {https://scholarship.rice.edu/handle/1911/62865},
  urldate = {2021-07-09},
  abstract = {Paper presented in three lectures in Anderson Hall on September 23, 24, 26, 1963},
  copyright = {All rights reserved by Rice University. This work is licensed under a Creative Commons Attribution Non-commercial 4.0 License.},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000723  Accepted: 2011-11-08T19:13:47Z}
}

@techreport{maslovReversibleLogicSynthesis2003,
  title = {Reversible {{Logic Synthesis}}},
  author = {Maslov, Dmitri},
  year = {2003},
  abstract = {at the University of New Brunswick, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. (Signature)}
}

@article{matsumoto1964generateurs,
  title = {G\'en\'erateurs et Relations Des Groupes de Weyl G\'en\'eralis\'es},
  author = {Matsumoto, Hideya},
  year = {1964},
  journal = {COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES},
  volume = {258},
  number = {13},
  pages = {3419},
  publisher = {{GAUTHIER-VILLARS/EDITIONS ELSEVIER 23 RUE LINOIS, 75015 PARIS, FRANCE}}
}

@inproceedings{melliesTemplateGamesDifferential2019,
  title = {Template Games and Differential Linear Logic},
  booktitle = {2019 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
  author = {Melli{\`e}s, Paul-Andr{\'e}},
  year = {2019},
  month = jun,
  pages = {1--13},
  doi = {10.1109/LICS.2019.8785830},
  abstract = {We extend our recent template game model of multiplicative additive linear logic (MALL) with an exponential modality of linear logic (LL) derived from the standard categorical construction Sym of the free symmetric monoidal category. We obtain in this way the first game semantics of differential linear logic (DiLL) in its classical form. The construction of the model relies on a careful and healthy comparison with the model of generalised species designed ten years ago by Fiore, Gambino, Hyland and Winskel. Besides the resolution of an old open problem of game semantics, the study reveals an unexpected and promising convergence between linear logic and homotopy theory.},
  keywords = {Additives,Cats,Games,Mathematical model,Semantics,Turning}
}

@inproceedings{millerTransformationBasedAlgorithm2003,
  title = {A Transformation Based Algorithm for Reversible Logic Synthesis},
  booktitle = {Proceedings 2003. {{Design Automation Conference}} ({{IEEE Cat}}. {{No}}.{{03CH37451}})},
  author = {Miller, D.M. and Maslov, D. and Dueck, G.W.},
  year = {2003},
  month = jun,
  pages = {318--323},
  doi = {10.1145/775832.775915},
  abstract = {A digital combinational logic circuit is reversible if it maps each input pattern to a unique output pattern. Such circuits are of interest in quantum computing, optical computing, nanotechnology and low-power CMOS design. Synthesis approaches are not well developed for reversible circuits even for small numbers of inputs and outputs. In this paper, a transformation based algorithm for the synthesis of such a reversible circuit in terms of n /spl times/ n Toffoli gates is presented. Initially, a circuit is constructed by a single pass through the specification with minimal look-ahead and no back-tracking. Reduction rules are then applied by simple template matching. The method produces very good results for larger problems.},
  keywords = {Circuit synthesis,Combinational circuits,Computer science,Logic design,Nanotechnology,Niobium,Optical computing,Optical design,Permission,Quantum computing}
}

@misc{molzerCubicalAgdaSimple2021,
  title = {Cubical {{Agda}}: Simple Application of {{Fin}}: Lehmer Codes},
  shorttitle = {Cubical {{Agda}}},
  author = {Molzer, Martin},
  year = {2021},
  month = nov,
  url = {https://github.com/agda/cubical/blob/a1d2bb38c0794f3cb00610cd6061cf9b5410518d/Cubical/Data/Fin/LehmerCode.agda},
  urldate = {2021-11-10},
  abstract = {An experimental library for Cubical Agda},
  copyright = {MIT},
  howpublished = {Agda Github Community}
}

@inproceedings{muInjectiveLanguageReversible2004,
  title = {An {{Injective Language}} for {{Reversible Computation}}},
  booktitle = {Mathematics of {{Program Construction}}},
  author = {Mu, Shin-Cheng and Hu, Zhenjiang and Takeichi, Masato},
  editor = {Kozen, Dexter},
  year = {2004},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {289--313},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/978-3-540-27764-4_16},
  abstract = {Erasure of information incurs an increase in entropy and dissipates heat. Therefore, information-preserving computation is essential for constructing computers that use energy more effectively. A more recent motivation to understand reversible transformations also comes from the design of editors where editing actions on a view need to be reflected back to the source data. In this paper we present a point-free functional language, with a relational semantics, in which the programmer is allowed to define injective functions only. Non-injective functions can be transformed into a program returning a history. The language is presented with many examples, and its relationship with Bennett's reversible Turing machine is explained. The language serves as a good model for program construction and reasoning for reversible computers, and hopefully for modelling bi-directional updating in an editor.},
  isbn = {978-3-540-27764-4},
  langid = {english},
  keywords = {Binary Tree,Functional Language,Injective Function,Relational Semantic,Turing Machine}
}

@inproceedings{ortonDecomposingUnivalenceAxiom2018,
  title = {Decomposing the {{Univalence Axiom}}},
  booktitle = {23rd {{International Conference}} on {{Types}} for {{Proofs}} and {{Programs}} ({{TYPES}} 2017)},
  author = {Orton, Ian and Pitts, Andrew M.},
  editor = {Abel, Andreas and Forsberg, Fredrik Nordvall and Kaposi, Ambrus},
  year = {2018},
  series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})},
  volume = {104},
  pages = {6:1--6:19},
  publisher = {{Schloss Dagstuhl\textendash Leibniz-Zentrum fuer Informatik}},
  address = {{Dagstuhl, Germany}},
  issn = {1868-8969},
  doi = {10.4230/LIPIcs.TYPES.2017.6},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/10054},
  urldate = {2021-10-26},
  isbn = {978-3-95977-071-2},
  keywords = {cubical sets,cubical type theory,dependent type theory,homotopy type theory,univalence,univalent type theory}
}

@article{peresReversibleLogicQuantum1985,
  title = {Reversible Logic and Quantum Computers},
  author = {Peres, Asher},
  year = {1985},
  month = dec,
  journal = {Physical Review A},
  volume = {32},
  number = {6},
  pages = {3266--3276},
  publisher = {{American Physical Society}},
  doi = {10.1103/PhysRevA.32.3266},
  url = {https://link.aps.org/doi/10.1103/PhysRevA.32.3266},
  urldate = {2021-11-10},
  abstract = {This article is concerned with the construction of a quantum-mechanical Hamiltonian describing a computer. This Hamiltonian generates a dynamical evolution which mimics a sequence of elementary logical steps. This can be achieved if each logical step is locally reversible (global reversibility is insufficient). Computational errors due to noise can be corrected by means of redundancy. In particular, reversible error-correcting codes can be embedded in the Hamiltonian itself. An estimate is given for the minimum amount of entropy which must be dissipated at a given noise level and tolerated error rate.}
}

@article{petrakisUnivalentTypoids2019,
  title = {Univalent Typoids},
  author = {Petrakis, I.},
  year = {2019},
  url = {https://www.math.lmu.de/~petrakis/Typoids.pdf},
  urldate = {2021-07-07},
  abstract = {A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equivalence relation between them, that generalise the properties of the equality terms. The resulting weak 2-groupoid structure can be extended to every finite level. The introduced notions of typoid and typoid function generalise the notions of setoid and setoid function. A univalent typoid is a typoid satisfying a general version of the univalence axiom. We prove some fundamental facts on univalent typoids, their product and exponential. As a corollary, we get an interpretation of propositional truncation within the theory of typoids. The couple typoid and univalent typoid is a weak groupoid-analogue to the couple precategory and category in homotopy type theory. 1998 ACM Subject Classification F.4.1 Mathematical Logic},
  langid = {english},
  annotation = {ZSCC: 0000000}
}

@inproceedings{piceghelloCoherenceMonoidalGroupoids2020,
  title = {Coherence for {{Monoidal Groupoids}} in {{HoTT}}},
  booktitle = {25th {{International Conference}} on {{Types}} for {{Proofs}} and {{Programs}} ({{TYPES}} 2019)},
  author = {Piceghello, Stefano},
  editor = {Bezem, Marc and Mahboubi, Assia},
  year = {2020},
  series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})},
  volume = {175},
  pages = {8:1--8:20},
  publisher = {{Schloss Dagstuhl\textendash Leibniz-Zentrum f\"ur Informatik}},
  address = {{Dagstuhl, Germany}},
  issn = {1868-8969},
  doi = {10.4230/LIPIcs.TYPES.2019.8},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/13072},
  urldate = {2021-07-07},
  isbn = {978-3-95977-158-0},
  keywords = {coherence,Coq,formalisation,groupoids,higher inductive types,homotopy type theory,monoidal categories},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{piceghelloCoherenceSymmetricMonoidal2019,
  title = {Coherence for Symmetric Monoidal Groupoids in {{HoTT}}/{{UF}}},
  author = {Piceghello, Stefano},
  year = {2019},
  pages = {2},
  url = {http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_10},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000003}
}

@misc{sabryJacquesCarettePidualSecond2021,
  title = {{{JacquesCarette}}/Pi-Dual: Second Alpha Release},
  shorttitle = {{{JacquesCarette}}/Pi-Dual},
  author = {Sabry, Amr and Carette, Jacques and {zsparks} and Chen, Chao-Hong and Choudhury, Vikraman and James, Roshan and {movieverse}},
  year = {2021},
  month = oct,
  doi = {10.5281/zenodo.5620828},
  url = {https://zenodo.org/record/5620828},
  urldate = {2021-10-30},
  abstract = {Should have done this release, for Zenodo, after flipping the switch.},
  howpublished = {Zenodo}
}

@article{shendeSynthesisReversibleLogic2003,
  title = {Synthesis of Reversible Logic Circuits},
  author = {Shende, V.V. and Prasad, A.K. and Markov, I.L. and Hayes, J.P.},
  year = {2003},
  month = jun,
  journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
  volume = {22},
  number = {6},
  pages = {710--722},
  issn = {1937-4151},
  doi = {10.1109/TCAD.2003.811448},
  abstract = {Reversible or information-lossless circuits have applications in digital signal processing, communication, computer graphics, and cryptography. They are also a fundamental requirement in the emerging field of quantum computation. We investigate the synthesis of reversible circuits that employ a minimum number of gates and contain no redundant input-output line-pairs (temporary storage channels). We prove constructively that every even permutation can be implemented without temporary storage using NOT, CNOT, and TOFFOLI gates. We describe an algorithm for the synthesis of optimal circuits and study the reversible functions on three wires, reporting the distribution of circuit sizes. We also study canonical circuit decompositions where gates of the same kind are grouped together. Finally, in an application important to quantum computing, we synthesize oracle circuits for Grover's search algorithm, and show a significant improvement over a previously proposed synthesis algorithm.},
  keywords = {Application software,Circuit synthesis,Computer graphics,Cryptography,Digital signal processing,Logic circuits,Quantum computing,Signal processing algorithms,Signal synthesis,Wires}
}

@article{sparksSuperstructuralReversibleLogic2014,
  title = {Superstructural {{Reversible Logic}}},
  author = {Sparks, Zachary and Sabry, Amr},
  year = {2014},
  pages = {12},
  url = {https://legacy.cs.indiana.edu/~sabry/papers/reversible-logic.pdf},
  abstract = {In some substructural logics, the memory used by proofs is treated as a first-class multiplicative resource, but the choices made by those proofs are not. Since we can convert between space and time complexity, these ``resource conscious'' logics are therefore not actually guaranteed to preserve memory\textemdash for example, linear logic allows the erasure and duplication of natural numbers with time complexity proportional to their size. In order to fully account for space-time tradeoffs, we augment contexts to track all information, not just multiplicative resources. This creates a reversible, fully resource-preserving logic which allows us to examine the hidden information effects in linear logic and study reversible computation from a proof-theoretic perspective.},
  langid = {english},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000007}
}

@book{spiwackConstructivelyFinite2010,
  title = {Constructively {{Finite}}?},
  author = {Spiwack, Arnaud and Coquand, Thierry},
  year = {2010},
  pages = {217},
  publisher = {{Universidad de La Rioja}},
  url = {https://hal.inria.fr/inria-00503917},
  urldate = {2021-07-06},
  abstract = {This articles plays with several properties of Bishop sets which would be equivalent in ZFC to being finite. One of which is new. This is an occasion to analyse finely the different properties of finite sets and how they (constructively) relate to one another. We close this article by presenting a few well-known algorithms on finite structures, and describe which kind of finiteness they require.},
  isbn = {978-84-96487-50-5},
  langid = {english},
  annotation = {ZSCC: 0000005}
}

@book{symmetryBook2021,
  title = {Symmetry},
  author = {Bezem, Marc and Buchholtz, Ulrik and Cagne, Pierre and Dundas, Bj{\o}rn Ian and Grayson, Daniel R.},
  year = {2021},
  month = oct,
  url = {https://github.com/UniMath/SymmetryBook},
  annotation = {ZSCC: NoCitationData[s0]}
}

@article{tabareauMarriageUnivalenceParametricity2021,
  title = {The {{Marriage}} of {{Univalence}} and {{Parametricity}}},
  author = {Tabareau, Nicolas and Tanter, {\'E}ric and Sozeau, Matthieu},
  year = {2021},
  month = jan,
  journal = {Journal of the ACM},
  volume = {68},
  number = {1},
  pages = {5:1--5:44},
  issn = {0004-5411},
  doi = {10.1145/3429979},
  url = {https://doi.org/10.1145/3429979},
  urldate = {2021-07-09},
  abstract = {Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity, is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport \`a la carte: basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.},
  keywords = {Coq,parametricity,proof assistants,Type equivalence,univalence},
  annotation = {ZSCC: 0000007}
}

@inproceedings{toffoliReversibleComputing1980,
  title = {Reversible Computing},
  booktitle = {Automata, {{Languages}} and {{Programming}}},
  author = {Toffoli, Tommaso},
  editor = {{de Bakker}, Jaco and {van Leeuwen}, Jan},
  year = {1980},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {632--644},
  publisher = {{Springer}},
  address = {{Berlin, Heidelberg}},
  doi = {10.1007/3-540-10003-2_104},
  abstract = {The theory of reversible computing is based on invertible primitives and composition rules that preserve invertibility. With these constraints, one can still satisfactorily deal with both functional and structural aspects of computing processes; at the same time, one attains a closer correspondence between the behavior of abstract computing systems and the microscopic physical laws (which are presumed to be strictly reversible) that underly any concrete implementation of such systems.According to a physical interpretation, the central result of this paper is that it is ideally possible to build sequential circuits with zero internal power dissipation.},
  isbn = {978-3-540-39346-7},
  langid = {english},
  keywords = {Causality Network,Cellular Automaton,Composition Rule,Finite Automaton,Turing Machine}
}

@book{univalentfoundationsprogramHomotopyTypeTheory2013,
  title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  author = {Univalent Foundations Program, The},
  year = {2013},
  publisher = {{Univalent Foundations Program}},
  address = {{Institute for Advanced Study}},
  url = {https://homotopytypetheory.org/book},
  annotation = {ZSCC: 0000005}
}

@article{vajnovszkiNewEulerMahonian2011,
  title = {A New {{Euler}}\textendash{{Mahonian}} Constructive Bijection},
  author = {Vajnovszki, Vincent},
  year = {2011},
  month = aug,
  journal = {Discrete Applied Mathematics},
  volume = {159},
  number = {14},
  pages = {1453--1459},
  issn = {0166-218X},
  doi = {10.1016/j.dam.2011.05.012},
  url = {http://www.sciencedirect.com/science/article/pii/S0166218X11001946},
  urldate = {2021-01-30},
  abstract = {Using generating functions, MacMahon proved in 1916 the remarkable fact that the major index has the same distribution as the inversion number for multiset permutations, and in 1968 Foata gave a constructive bijection proving MacMahon's result. Since then, many refinements have been derived, consisting of adding new constraints or new statistics. Here we give a new simple constructive bijection between the set of permutations with a given number of inversions and those with a given major index. We introduce a new statistic, mix, related to the Lehmer code, and using our new bijection we show that the bistatistic (mix,INV) is Euler\textendash Mahonian. Finally, we introduce the McMahon code for permutations which is the major-index counterpart of the Lehmer code and show that the two codes are related by a simple relation.},
  langid = {english},
  keywords = {Constructive bijection,Inversion number,Major index,Permutation (bi)statistic},
  annotation = {ZSCC: 0000011}
}

@article{vantonderLambdaCalculusQuantum2004,
  title = {A {{Lambda Calculus}} for {{Quantum Computation}}},
  author = {{van Tonder}, Andr{\'e}},
  year = {2004},
  month = jan,
  journal = {SIAM Journal on Computing},
  volume = {33},
  number = {5},
  pages = {1109--1135},
  publisher = {{Society for Industrial and Applied Mathematics}},
  issn = {0097-5397},
  doi = {10.1137/S0097539703432165},
  url = {https://epubs.siam.org/doi/10.1137/S0097539703432165},
  urldate = {2021-11-10},
  abstract = {The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of linear logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.},
  keywords = {03B70,68N18,68Q10,81P68,lambda calculus,linear logic,models of computation,quantum computation}
}

@article{vezzosiCubicalAgdaDependently2019,
  title = {Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types},
  shorttitle = {Cubical Agda},
  author = {Vezzosi, Andrea and M{\"o}rtberg, Anders and Abel, Andreas},
  year = {2019},
  month = jul,
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  pages = {87:1--87:29},
  doi = {10.1145/3341691},
  url = {https://doi.org/10.1145/3341691},
  urldate = {2021-06-29},
  abstract = {Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.},
  keywords = {Cubical Type Theory,Dependent Pattern Matching,Higher Inductive Types,Univalence},
  annotation = {ZSCC: 0000002}
}

@article{yanofskySyntaxCoherence2000,
  title = {{The syntax of coherence}},
  author = {Yanofsky, Noson S.},
  year = {2000},
  journal = {Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle Cat\'egoriques},
  volume = {41},
  number = {4},
  pages = {255--304},
  url = {http://www.numdam.org/item/?id=CTGDC_2000__41_4_255_0},
  urldate = {2021-06-12},
  langid = {french},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000004}
}

@inproceedings{yokoyamaPrinciplesReversibleProgramming2008,
  title = {Principles of a Reversible Programming Language},
  booktitle = {Proceedings of the 5th Conference on {{Computing}} Frontiers},
  author = {Yokoyama, Tetsuo and Axelsen, Holger Bock and Gl{\"u}ck, Robert},
  year = {2008},
  month = may,
  series = {{{CF}} '08},
  pages = {43--54},
  publisher = {{Association for Computing Machinery}},
  address = {{New York, NY, USA}},
  doi = {10.1145/1366230.1366239},
  url = {https://doi.org/10.1145/1366230.1366239},
  urldate = {2021-11-10},
  abstract = {The principles of reversible programming languages are explicated and illustrated with reference to the design of a high-level imperative language, Janus. The fundamental properties for such languages include backward as well as forward determinism and reversible updates of data. The unique design features of the language include explicit post-condition assertions, direct access to an inverse semantics and the possibility of clean (\{\textbackslash ie\}, garbage-free) computation of injective functions. We suggest the clean simulation of reversible Turing machines as a criterion for computing strength of reversible languages, and demonstrate this for Janus. We show the practicality of the language by implementation of a reversible fast Fourier transform. Our results indicate that the reversible programming paradigm has fundamental properties that are relevant to many different areas of computer science.},
  isbn = {978-1-60558-077-7},
  keywords = {backward determinism,fast fourier transform,inverse semantics,reversible computing,turing completeness}
}

@inproceedings{yokoyamaReversibleProgrammingLanguage2007,
  title = {A Reversible Programming Language and Its Invertible Self-Interpreter},
  booktitle = {Proceedings of the 2007 {{ACM SIGPLAN}} Symposium on {{Partial}} Evaluation and Semantics-Based Program Manipulation},
  author = {Yokoyama, Tetsuo and Gl{\"u}ck, Robert},
  year = {2007},
  month = jan,
  series = {{{PEPM}} '07},
  pages = {144--153},
  publisher = {{Association for Computing Machinery}},
  address = {{New York, NY, USA}},
  doi = {10.1145/1244381.1244404},
  url = {https://doi.org/10.1145/1244381.1244404},
  urldate = {2021-11-10},
  abstract = {A reversible programming language supports deterministic forward and backward computation. We formalize the programming language Janus and prove its reversibility. We provide a program inverter for the language and implement a self-interpreter that achieves deterministic forward and backward interpretation of Janus programs without using a computation history. As the self-interpreter is implemented in a reversible language, it is invertible using local program inversion. Many physical phenomena are reversible and we demonstrate the power of Janus by implementing a reversible program for discrete simulation of the Schr\"odinger wave equation that can be inverted as well as run forward and backward.},
  isbn = {978-1-59593-620-2},
  keywords = {Janus,non-standard interpreter hierarchy,program inversion,reversible computing,reversible programming language,self-interpreter}
}

@article{yorgeyCombinatorialSpeciesLabelled2014,
  title = {Combinatorial Species and Labelled Structures},
  author = {Yorgey, Brent Abraham},
  year = {2014},
  month = jan,
  journal = {Dissertations available from ProQuest},
  pages = {1--206},
  url = {https://repository.upenn.edu/dissertations/AAI3668177},
  keywords = {⛔ No DOI found},
  annotation = {ZSCC: 0000013}
}