Topological quantum gates in homotopy type theory. (English) Zbl 07893326
Summary: Despite the plausible necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their physical realization as well as their information-theoretic nature. Building on recent results on defect branes in string/M-theory (Sati and Schreiber in Rev Math Phys, 2023. doi:10.1142/S0129055X23500095. [arXiv:2203.11838]) and on their holographically dual anyonic defects in condensed matter theory (Sati and Schreiber in Rev Math Phys 35(03):2350001, 2023. doi:10.1142/S0129055X23500010. [arXiv:2206.13563]), here we explain [as announced in Sati and Schreiber (PlanQC 2022:33, 2022, [arXiv:2209.08331], [ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K])] how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages, such as cubical Agda. We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper as well as of real-world application of homotopy type theory, both of which have arguably been falling behind their high expectations; in any case, it provides a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware. In companion articles (Sati and Schreiber in The Quantum Monadology, [arXiv:2310.15735], Sati and Schreiber in Entanglement of Sections: The pushout of entangled and parameterized quantum information [arXiv:2309.07245]) [announced in Schreiber (Quantum types via Linear Homotopy Type Theory, talk at Workshop on Quantum Software @ QTML2022, Naples, 2022, [ncatlab.org/schreiber/files/QuantumDataInLHoTT-221117.pdf])], we explain how further passage to “dependent linear” homotopy types naturally extends this scheme to a full-blown quantum programming/certification language in which our topological quantum gates may be compiled to verified quantum circuits, complete with quantum measurement gates and classical control.
MSC:
| 03Bxx | General logic |
| 81Txx | Quantum field theory; related classical field theories |
| 81Pxx | Foundations, quantum information and its processing, quantum axioms, and philosophy |
References:
| [1] | Abad, CA, Introduction to representations of braid groups, Rev. Colomb. Mat., 49, 1, 1, 2015 · Zbl 1365.20037 · doi:10.15446/recolma.v49n1.54160 |
| [2] | Aczel, P.: On Voevodsky’s Univalence Axiom, talk at the Third European Set Theory Conference (2011), [ncatlab.org/nlab/files/Aczel-Univalence.pdf] |
| [3] | Adamek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories, John Wiley and Sons, New York (1990); reprinted as: Reprints in Th. Appl. Categ. 17, 1-507, (2006), [tac:tr17] · Zbl 1113.18001 |
| [4] | Adams, J.F.: Stable homotopy and generalized homology, Chicago Lectures in Math., University of Chicago Press, 1974, [ucp:bo21302708] · Zbl 0309.55016 |
| [5] | Adams, JF, Infinite Loop Spaces, Annals of Mathematics Studies, 1978, Princeton: Princeton University Press, Princeton · Zbl 0398.55008 · doi:10.1515/9781400821259 |
| [6] | Aguilar, M.; Gitler, S.; Prieto, C., Algebraic Topology from a Homotopical Viewpoint, 2002, Berlin: Springer, Berlin · Zbl 1006.55001 · doi:10.1007/b97586 |
| [7] | Aharonov, D., van Dam, W., Kempe, J., Landau, Z., Lloyd, S., Regev, O.: Adiabatic quantum computation is equivalent to standard quantum computation, SIAM J. Comput. 37 1 (2007), 166-194 · Zbl 1134.81009 |
| [8] | Aharony, O.; Gubser, S.; Maldacena, J.; Ooguri, H.; Oz, Y., Large \(N\) field theories, string theory and gravity, Phys. Rep., 323, 183-386, 2000 · Zbl 1368.81009 · doi:10.1016/S0370-1573(99)00083-6 |
| [9] | Ahrens, B., North, P.R.: Univalent foundations and the equivalence principle. In: Reflections on the Foundations of Mathematics, Synthese Library 407, Springer, Berlin (2019), doi:10.1007/978-3-030-15655-8, arXiv:2202.01892 · Zbl 1528.03101 |
| [10] | Ahrens, B., North, P.R., Shulman, M., Tsementzis, D.: A Higher Structure Identity Principle, LICS ‘20 (2020), 53-66, doi:10.1145/3373718.3394755, arXiv:2004.06572 · Zbl 1498.03027 |
| [11] | Aman, B., Ciobanu, G., Glück, R., Kaarsgaard, R., Kari, J., Kutrib, M., Lanese, I., Antares Mezzina, C., Mikulski, Ł., Nagarajan, R., Phillips, I., Pinna, G.M., Prigioniero, L., Ulidowski, I., Vidal, G.: Foundations of Reversible Computation, in: Reversible Computation: Extending Horizons of Computing. RC 2020, Lec. Notes Comp. Sci. 12070, Springer, New York (2020), doi:10.1007/978-3-030-47361-7_1 |
| [12] | Anderson, F.W., Fuller, K.R.: Rings and Categories of Modules, Graduate Texts in Mathematics 13 Springer. Berlin (1992). doi:10.1007/978-1-4612-4418-9 · Zbl 0765.16001 |
| [13] | Ando, M.; Blumberg, A.; Gepner, D.; Hopkins, M.; Rezk, C., An \(\infty \)-categorical approach to \(R\)-line bundles, R \(R\)-module Thom spectra, and twisted \(R\)-homology, J. Topology, 7, 3, 869-893, 2014 · Zbl 1312.55011 · doi:10.1112/jtopol/jtt035 |
| [14] | Arkowitz, M., Introduction to Homotopy Theory, 2011, Berlin: Springer, Berlin · Zbl 1232.55001 · doi:10.1007/978-1-4419-7329-0 |
| [15] | Artin, E., Theorie der Zöpfe, Abh. Math. Semin. Univ. Hambg., 4, 47-72, 1925 · JFM 51.0450.01 · doi:10.1007/BF02950718 |
| [16] | Avron, JE; Seiler, R.; Yaffe, LG, Adiabatic theorems and applications to the quantum Hall effect, Commun. Math. Phys., 110, 33-49, 1987 · Zbl 0626.58033 · doi:10.1007/BF01209015 |
| [17] | Awodey, S.: Type theory and homotopy, In: Epistemology versus Ontology, Springer, Berlin (2012), 183-201, doi:10.1007/978-94-007-4435-6_9, arXiv:1010.1810 · Zbl 1314.03013 |
| [18] | Awodey, S.: Natural Models of Homotopy Type Theory (Abstract). in: Logic, Language, Information, and Computation. WoLLIC 2013. Lecture Notes in Computer Science 8071, Springer, Berlin, Heidelberg. doi:10.1007/978-3-642-39992-3_2arXiv:1406.3219 (2013) |
| [19] | Awodey, S.; Bauer, A., Propositions as [Types], J. Logic Comput., 14, 447-471, 2004 · Zbl 1050.03016 · doi:10.1093/logcom/14.4.447 |
| [20] | Awodey, S., Gambino, N., Sojakova, K.: Inductive types in homotopy type theory, LICS’12 (2012), 95-104, doi:10.1109/LICS.2012.21, arXiv:1201.3898 · Zbl 1364.03014 |
| [21] | Awodey, S.; Gambino, N.; Sojakova, K., Homotopy-initial algebras in type theory, J. Assoc. Comput. Mach., 636, 1-45, 2017 · Zbl 1426.03016 · doi:10.1145/3006383 |
| [22] | Awodey, S.; Warren, M., Homotopy theoretic models of identity type, Math. Proc., 146, 45-55, 2009 · Zbl 1205.03065 · doi:10.1017/S0305004108001783 |
| [23] | Bachmann, S., De Roeck, W., Fraas, M.: The adiabatic theorem in a quantum many-body setting. In: Analytic Trends in Mathematical Physics, Cont. Math. 741, 43-58, (2020), [ams:conm-741], arXiv:1808.09985 · Zbl 1446.82043 |
| [24] | Bailey, D.; Borwein, P.; Plouffe, S., On the rapid computation of various polylogarithmic constants, Math. Comp., 66, 903-913, 1997 · Zbl 0879.11073 · doi:10.1090/S0025-5718-97-00856-9 |
| [25] | Balmer, P., Stacks of group representations, J. Eur. Math. Soc., 17, 1, 189-228, 2015 · Zbl 1351.20004 · doi:10.4171/jems/501 |
| [26] | Barthe, G.; Capretta, V.; Pons, O., Setoids in type theory, J. Funct. Progr., 13, 2, 261-293, 2003 · Zbl 1060.03030 · doi:10.1017/S0956796802004501 |
| [27] | Barthe, G., Pons, O.: Type Isomorphisms and Proof Reuse in Dependent Type Theory, in: Foundations of Software Science and Computation Structures. FoSSaCS 2001, Lecture Notes in Computer Science 2030, Springer, Berlin (2001), doi:10.1007/3-540-45315-6_4 · Zbl 0978.68044 |
| [28] | Baues, H.J.: Homotopy Types in Handbook of Algebraic Topology, North Holland (1995), 1-72, doi:10.1016/B978-0-444-81779-2.X5000-7, [ncatlab.org/nlab/files/Baues-HomotopyTypes.pdf] · Zbl 0869.55006 |
| [29] | Benenti, G., Casati, G., Rossini, D.: Principles of Quantum Computation and Information, World Scientific, Singapore (2004, 2018), doi:10.1142/10909 · Zbl 1496.81014 |
| [30] | Benioff, P., The computer as a physical system: a microscopic quantum mechanical Hamiltonian model of computers as represented by Turing machines, J. Stat. Phys., 22, 563-591, 1980 · Zbl 1382.68066 · doi:10.1007/BF01011339 |
| [31] | Bennett, CH, Notes on Landauer’s principle, reversible computation, and Maxwell’s Demon, Stud. Hist. Philos. Mod. Phys., 34, 3, 501-510, 2003 · Zbl 1222.81039 · doi:10.1016/S1355-2198(03)00039-X |
| [32] | Berry, MV, Quantal phase factors accompanying adiabatic changes, Proc. R. Soc. Lond. A, 392, 45-57, 1984 · Zbl 1113.81306 · doi:10.1098/rspa.1984.0023 |
| [33] | Berry, M.: The quantum phase, five years after, In: Geometric phases in physics, Adv. Ser. Math. Phys. 5, World Scientific (1989), 7-28, doi:10.1142/0613 |
| [34] | Bezem, M., Buchholtz, U., Cagne, P., Dundas, B.I., Grayson, D.R.: Symmetry (2021), [unimath.github.io/SymmetryBook/book.pdf], [github.com/UniMath/agda-unimath/tree/master/src/group-theory] |
| [35] | Birkhoff, G.; von Neumann, J., The logic of quantum mechanics, Ann. Math., 37, 823-843, 1936 · Zbl 0015.14603 · doi:10.2307/1968621 |
| [36] | Birman, JS, Braids, Links, and Mapping Class Groups, 1975, Princeton: Princeton University Press, Princeton · Zbl 0305.57013 · doi:10.1515/9781400881420 |
| [37] | Bishop, E.: Foundations of Constructive Analysis, McGraw-Hill (1967), [archive.org/details/foundationsofcon0000bish] · Zbl 0183.01503 |
| [38] | Bishop, E.; Bridges, D., Constructive Analysis, 1985, Berlin: Springer, Berlin · Zbl 0656.03042 · doi:10.1007/978-3-642-61667-9 |
| [39] | Bland, P.E.: Rings and Their Modules. De Gruyter. Berlin (2011). doi:10.1515/9783110250237 · Zbl 1217.16001 |
| [40] | Bohannon, A., Pierce, B.C., Vaughan, J.A.: Relational lenses: a language for updatable views, Proceedings of Principles of Database Systems (2006), 338-347, doi:10.1145/1142351.1142399 |
| [41] | Bonesteel, NE; Hormozi, L.; Zikos, G.; Simon, SH, Braid topologies for quantum computation, Phys. Rev. Lett., 95, 2005 · doi:10.1103/PhysRevLett.95.140503 |
| [42] | Booth, P.I.: The Exponential Law of Maps I, Proc. London Math. Soc. s3-20 (1970), 179-192, doi:10.1112/plms/s3-20.1.179 · Zbl 0189.54301 |
| [43] | Booth, PI; Brown, R., Spaces of partial maps, fibred mapping spaces and the compact-open topology, Gen. Topol. Appl., 8, 181-195, 1978 · Zbl 0373.54012 · doi:10.1016/0016-660X(78)90049-1 |
| [44] | Borceux, F., Categories and Structures, Vol. 2 of: Handbook of Categorical Algebra, Enc. Math. Appl., 1994, Cambridge: Cambridge University Press, Cambridge · Zbl 0911.18001 · doi:10.1017/CBO9780511525865 |
| [45] | Borceux, F., Categories of Sheaves, Vol. 3 of: Handbook of Categorical Algebra, Enc. Math. Appl., 1994, Cambridge: Cambridge University Press, Cambridge · Zbl 0911.18001 · doi:10.1017/CBO9780511525872 |
| [46] | Bouwmeester, D., Ekert, A., Zeilinger, A.: The Physics of Quantum Information-Quantum Cryptography, Quantum Teleportation, Quantum Computation. Springer, New York (2020). doi:10.1007/978-3-662-04209-0 · Zbl 1008.81504 |
| [47] | Braunack-Mayer, V., Combinatorial parametrised spectra, Algebr. Geom. Topol., 21, 801-891, 2021 · Zbl 1498.55009 · doi:10.2140/agt.2021.21.801 |
| [48] | Bredon, G.: Topology and Geometry, Graduate Texts in Math. 139, Springer, Berlin (1993), doi:10.1007/978-1-4757-6848-0 · Zbl 0791.55001 |
| [49] | Brennen, GK; Pachos, JK, Why should anyone care about computing with anyons?, Proc. R. Soc. A, 464, 1-24, 2008 · Zbl 1132.81004 · doi:10.1098/rspa.2007.0026 |
| [50] | Bridges, D., Constructive mathematics: a foundation for computable analysis, Theor. Comp Sci., 219, 1-2, 95-109, 1999 · Zbl 0916.68048 · doi:10.1016/S0304-3975(98)00285-0 |
| [51] | Brown, EH Jr, Abstract homotopy theory, Trans. Am. Math. Soc., 119, 79-85, 1965 · Zbl 0129.15301 · doi:10.1090/S0002-9947-1965-0182970-6 |
| [52] | Brown, K.S.: Abstract Homotopy Theory and Generalized Sheaf Cohomology, Trans. Amer. Math. Soc., 186, 419-458, (1973) [jstor:1996573] · Zbl 0245.55007 |
| [53] | Brunekreef, J.W.: Topological Quantum Computation and Quantum Compilation, thesis, Utrecht (2014), [studentheses:20.500.12932/17738] |
| [54] | Brunerie, G., Licata, D., Lumsdaine, P.: Homotopy theory in type theory, lecture notes (2013), [dlicata.wescreates.wesleyan.edu/pubs/bll13homotopy/bll13homotopy.pdf] · Zbl 1427.03033 |
| [55] | Brunerie, G., Ljungström, A., Mörtberg, A.: Synthetic Integral Cohomology in Cubical Agda. In: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) 216 (2022), doi:10.4230/LIPIcs.CSL.2022.11 · Zbl 1541.03031 |
| [56] | Buchholtz, U., Christensen, J.D., Taxerás Flaten, J., Rijke, E.: Central H-spaces and banded types, [arXiv:2301.02636] |
| [57] | Buchholtz, U.; van Doorn, F.; Rijke, E., Higher groups in homotopy type theory, LICS, 33, 205-214, 2018 · Zbl 1452.03034 · doi:10.1145/3209108.3209150 |
| [58] | Bunge, M.: Possibility and Probability. In: Foundations of Probability Theory, Statistical Interference, and Statistical Theories of Science, Reidel Publishing, pp. 17-34 (1976), doi:10.1007/978-94-010-1438-0_2 |
| [59] | Bunke, U.; Nikolaus, T.; Völkl, M., Differential cohomology theories as sheaves of spectra, J. Homotopy Rel. Struct., 11, 1-66, 2016 · Zbl 1341.57020 · doi:10.1007/s40062-014-0092-5 |
| [60] | Cabra, DC; Rossini, GL, Explicit connection between conformal field theory and 2+1 Chern-Simons theory, Mod. Phys. Lett. A, 12, 1687-1697, 1997 · Zbl 0901.53062 · doi:10.1142/S0217732397001722 |
| [61] | Cagliari, F.; Mantovani, S.; Vitale, E., Regularity of the category of Kelley spaces, Appli. Categ. Struc., 3, 357-361, 1995 · Zbl 0840.18002 · doi:10.1007/BF00872904 |
| [62] | Cattaneo, A.; Giaquinto, A.; Xu, P., Higher Structures in Geometry and Physics - In Honor of Murray Gerstenhaber and Jim Stasheff, Progress in Mathematics 287, Birkhäuser, 2001 · Zbl 1203.00021 · doi:10.1007/978-0-8176-4735-3 |
| [63] | Cavallo, E.: Synthetic Cohomology in Homotopy Type Theory., PhD Thesis, Carnegie Mellon University (2015), [staff.math.su.se/evan.cavallo/works/thesis15.pdf] |
| [64] | Cesare, C.; Landahl, AJ; Bacon, D.; Flammia, ST; Neels, A., Adiabatic topological quantum computing, Phys. Rev. A, 92, 2015 · doi:10.1103/PhysRevA.92.012336 |
| [65] | Cheng, M.; Galitski, V.; Das Sarma, S., Non-adiabatic Effects in the Braiding of Non-Abelian Anyons in Topological Superconductors, Phys. Rev. B, 84, 104529, 2011 · doi:10.1103/PhysRevB.84.104529 |
| [66] | Cherubini, F.; Rijke, E., Modal descent, Math. Struc. Comput. Sci., 31, 4, 2021 · Zbl 1481.18029 · doi:10.1017/S0960129520000201 |
| [67] | Childs, A.; Farhi, E.; Preskill, J., Robustness of adiabatic quantum computation, Phys. Rev. A, 65, 2002 · doi:10.1103/PhysRevA.65.012322 |
| [68] | Chlipala, A.: Implementing Certified Programming Language Tools in Dependent Type Theory, PhD thesis, U. California at Berkeley (2007), [UCB/EECS-2007-113] |
| [69] | Chlipala, A.: Certified programming with dependent types, MIT Press, Boston (2013), [ISBN:9780262026659] · Zbl 1288.68001 |
| [70] | Church, A., A formulation of the simple theory of types, J. Symbolic Logic, 5, 2, 56-68, 1940 · JFM 66.1192.06 · doi:10.2307/2266170 |
| [71] | Cisinski, D.-C.: Cambridge University Press. (2019). doi:10.1017/9781108588737 · Zbl 1430.18001 |
| [72] | Clarke, J.; Wilhelm, FK, Superconducting quantum bits, Nature, 453, 1031-1042, 2008 · doi:10.1038/nature07128 |
| [73] | Coen, C.S., Tassi, E.: Working with Mathematical Structures in Type Theory, in: Types for Proofs and Programs. TYPES 2007, Lecture Notes in Computer Science 4941 Springer (2008), doi:10.1007/978-3-540-68103-8_11 |
| [74] | Cohen, F.R.: Introduction to configuration spaces and their applications, In: Braids, Lecture Notes Series, Institute for Mathematical Sciences, 19, 183-261. World Scientific, Singapore (2009) · Zbl 1204.55001 |
| [75] | Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical Type Theory: a constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs (TYPES 2015), 5.1-5.34, Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany doi:10.48550/arXiv.1611.02108 · Zbl 1434.03036 |
| [76] | Coquand, T.: Equality and dependent type theory, lecture notes (2011), [ncatlab.org/nlab/files/Coquand-EqualityAndDependentTypeTheory.pdf] |
| [77] | Coquand, T.; Danielsson, NA, Isomorphism is equality, Indag. Math., 24, 4, 1105-1120, 2013 · Zbl 1359.03010 · doi:10.1016/j.indag.2013.09.002 |
| [78] | Coquand, Thierry, Huber, Simon, Mörtberg, Anders: On Higher Inductive Types in Cubical Type Theory, in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18) (2018), Association for Computing Machinery, New York, NY, USA, pp. 255-264. doi:10.1145/3209108.3209197 · Zbl 1452.03036 |
| [79] | Coquand, T., Paulin, C.: Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer, Berlin (1990), pp. 50-66, doi:10.1007/3-540-52335-9_47 · Zbl 0722.03006 |
| [80] | Coquand, T., Spiwack, A.: Towards constructive homological algebra in type theory, in: Towards Mechanized Mathematical Assistants. MKM Calculemus 2007, Lecture Notes in Computer Science 4573 Springer, Berlin (2007), doi:10.1007/978-3-540-73086-6_4 · Zbl 1202.68376 |
| [81] | O’Connor, R.; Monadic, A., Functional Implementation of Real Numbers, Math. Struc. Comput. Sci., 17, 1, 129-159, 2007 · Zbl 1121.03024 · doi:10.1017/S0960129506005871 |
| [82] | Constable, R.: The Triumph of Types: Creating a Logic of Computational Reality, lecture at: Types, Semantics and Verification, Oregon (2011), [www.cs.uoregon.edu/research/summerschool/summer11/lectures/Triumph-of-Types-Extended.pdf] |
| [83] | Corfield, D., Sati, H., Schreiber, U.: Fundamental weight systems are quantum states, [arXiv:2105.02871] · Zbl 1538.81003 |
| [84] | Corry, L., Modern Algebra and the Rise of Mathematical Structures, Springer. Berlin, 2004 · Zbl 1044.01008 · doi:10.1007/978-3-0348-7917-0 |
| [85] | Corry, L.: A Brief History of Numbers, Oxford University Press (2015), [ISBN:9780198702597] · Zbl 1335.01001 |
| [86] | Cory, D.G., Laflamme, R., Knill, E., Viola, L., Havel, T.F., Boulant, N., Boutis, G., Fortunato, E., Lloyd, S., Martinez, R., Negrevergne, C., Pravia, M., Sharf, Y., Teklemariam, G., Weinstein, Y.S., Zurek, W.H.: NMR Based Quantum Information Processing: Achievements and Prospects, Fortsch. Phys. 48 (2000), 875-907, [arXiv:quant-ph/0004104], https://doi.org/10.1002/1521-3978(200009)48:\(9/11<875\)::AID-PROP \(875>3.0\).CO;2-V |
| [87] | Crabb, M.C., James, I.M.: Fiberwise Homotopy Theory. Springer, Berlin (1998). doi:10.1007/978-1-4471-1265-5 · Zbl 0905.55001 |
| [88] | Curien, P-L; Garner, R.; Hofmann, M., Revisiting the categorical interpretation of dependent type theory, Theor. Comput. Sci., 546, 21, 99-119, 2014 · Zbl 1433.03029 · doi:10.1016/j.tcs.2014.03.003 |
| [89] | Das Sarma, S.: Quantum computing has a hype problem, MIT Technology Review (March 2022), [www.technologyreview.com/2022/03/28/1048355/quantum-computing-has-a-hype-problem] |
| [90] | Das Sarma, S.: In search of Majorana, [arXiv:2210.17365] |
| [91] | Das Sarma, S., Pan, H.: Disorder-induced zero-bias peaks in Majorana nanowires, Phys. Rev. B 103 (2021) 195158, doi:10.1103/PhysRevB.103.195158, [arXiv:2103.05628] |
| [92] | Date, E.; Jimbo, M.; Matsuo, A.; Miwa, T., Hypergeometric-type integrals and the \(\mathfrak{sl} (2,\mathbb{C} )\) Knizhnik-Zamolodchikov equation, Int. J. Mod. Phys. B, 4, 5, 1049-1057, 1990 · Zbl 0722.33007 · doi:10.1142/S0217979290000528 |
| [93] | Dawson, C.M., Nielsen, M.A.: The Solovay-Kitaev algorithm. Quantum Info. Comput. 6(1), 81-95 (2006). doi:10.5555/2011679.2011685. [arXiv:quant-ph/0505030] · Zbl 1152.81706 |
| [94] | de Bruijn, N., Telescopic mappings in typed lambda calculus, Inf. Comput., 91, 2, 189-204, 1991 · Zbl 0723.68024 · doi:10.1016/0890-5401(91)90066-B |
| [95] | Deligne, P.: Equations différentielles à points singuliers règuliers, Lect. Notes Math. 163 Springer (1970), [ias:355] · Zbl 0244.14004 |
| [96] | Deutsch, DE, Quantum computational networks, Proc. R. Soc. A, 425, 1868, 73-90, 1989 · Zbl 0691.68054 · doi:10.1098/rspa.1989.0099 |
| [97] | Di Cosmo, R., Isomorphisms of Types - from \(\lambda \)-calculus to information retrieval and language design, Progress Theor. Comput. Sci., 1995 · Zbl 0819.03006 · doi:10.1007/978-1-4612-2572-0 |
| [98] | Di Francesco, P.; Mathieu, P.; Sénéchal, D., Conformal Field Theory, 1997, Berlin: Springer, Berlin · Zbl 0869.53052 · doi:10.1007/978-1-4612-2256-9 |
| [99] | Dimca, A., Sheaves in Topology, 2004, Berlin: Springer, Berlin · Zbl 1043.14003 · doi:10.1007/978-3-642-18868-8 |
| [100] | Ding, M., Roberts, C.D., Schmidt, S.M.: Emergence of Hadron Mass and Structure, [arXiv:2211.07763] |
| [101] | Downen, P.; Ariola, ZM, A tutorial on computational classical logic and the sequent calculus, J. Funct. Progr., 28, E3, 2018 · doi:10.1017/S0956796818000023 |
| [102] | Dowling, MR; Nielsen, MA, The geometry of quantum computation, Quant. Info. Comput., 8, 10, 861-899, 2008 · Zbl 1158.81313 · doi:10.5555/2016985.2016986 |
| [103] | Duff, M.: The World in Eleven Dimensions: Supergravity, Supermembranes and M-theory, IoP, Bristol (1999), [ISBN:9780750306720] · Zbl 0999.00513 |
| [104] | Dwyer, W., Spalinski, J.: Homotopy theories and model categories. In: I. M. James (ed.), Handbook of Algebraic Topology, North Holland (1995), doi:10.1016/B978-0-444-81779-2.X5000-7 · Zbl 0869.55018 |
| [105] | Dybjer, P., Inductive families, Formal Aspects Comput., 6, 440-465, 1994 · Zbl 0808.03044 · doi:10.1007/BF01211308 |
| [106] | Dybjer, P.: Internal Type Theory, Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science 1158 Springer (1995) doi:10.1007/3-540-61780-9_66 |
| [107] | Dybjer, P., Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theor. Comput. Sci., 176, 1-2, 329-335, 1997 · Zbl 0898.68047 · doi:10.1016/S0304-3975(96)00145-4 |
| [108] | Equbal, A.: Molecular spin qubits for future quantum technology, Quantum Colloquium at CQTS (Nov 2022), [ncatlab.org/nlab/show/CQTS#EqubalNov22] |
| [109] | Erlich, J., An Introduction to Holographic QCD for Nonspecialists, Contemp. Phys., 56, 2, 2015 · doi:10.1080/00107514.2014.942079 |
| [110] | Escardó, M.H.: Introduction to Univalent Foundations of Mathematics with Agda (2019), [arXiv:1911.00580], [cs.bham.ac.uk/\( \sim\) mhe/HoTT-UF-in-Agda-Lecture-Notes] |
| [111] | Etingof, P.I., Frenkel, I., Kirillov, A.A.: Lectures on Representation Theory and Knizhnik-Zamolodchikov Equations, Math. Surv. monogr. 58, Amer. Math. Soc., Providence, RI (1998), [ams.org/surv-58] · Zbl 0903.17006 |
| [112] | Fadell, E.; Neuwirth, L., Configuration spaces, Math. Scand., 10, 111-118, 1962 · Zbl 0136.44104 · doi:10.7146/math.scand.a-10517 |
| [113] | Fadell, E., Husseini, S.: Geometry and topology of configuration spaces. Springer, Berlin (2001). doi:10.1007/978-3-642-56446-8 · Zbl 0962.55001 |
| [114] | Farhi, E., Goldstone, J., Gutmann, S., Sipser, M.: Quantum Computation by Adiabatic Evolution, [arXiv:quant-ph/0001106] · Zbl 1187.81063 |
| [115] | Feynman, R., Simulating physics with computers, Int. J. Theor. Phys., 21, 467-488, 1982 · doi:10.1007/BF02650179 |
| [116] | Feigin, B., Schechtman, V., Varchenko, A.: On algebraic equations satisfied by hypergeometric correlators in WZW models. I, Commun. Math. Phys. 163 (1994), 173-184, doi:10.1007/BF02101739 · Zbl 0835.17019 |
| [117] | Fiorenza, D.; Sati, H.; Schreiber, U., The rational higher structure of M-theory, Fortsch. Phys., 67, 1910017, 2019 · Zbl 1535.81196 · doi:10.1002/prop.201910017 |
| [118] | Fiorenza, D.; Sati, H.; Schreiber, U., The Character Map in Non-Abelian Cohomology-Twisted, Differential and Generalized, World Scientific, 2023 · Zbl 07707193 · doi:10.1142/13422 |
| [119] | Fox, RH; Neuwirth, L., The braid groups, Math. Scand., 10, 119-126, 1962 · Zbl 0117.41101 · doi:10.7146/math.scand.a-10518 |
| [120] | Freed, DS; Moore, GW, Twisted equivariant matter, Ann. Henri Poincaré, 14, 1927-2023, 2013 · Zbl 1286.81109 · doi:10.1007/s00023-013-0236-x |
| [121] | Freedman, M., P/NP, and the quantum field-computer, Proc. Nat. Acad. Sci., 95, 1, 98-101, 1998 · Zbl 0895.68053 · doi:10.1073/pnas.95.1.9 |
| [122] | Freedman, MH; Larsen, M.; Wang, Z., A modular functor which is universal for quantum computation, Commun. Math. Phys., 227, 605-622, 2002 · Zbl 1012.81007 · doi:10.1007/s002200200645 |
| [123] | Freedman, M.; Kitaev, A.; Larsen, M.; Wang, Z., Topological Quantum Computation, Bull. Am. Math. Soc., 40, 31, 2003 · Zbl 1019.81008 · doi:10.1090/S0273-0979-02-00964-3 |
| [124] | Frege, G.: Begriffsschrift:eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert (1879), [ISBN:9783487006239]; English translation: J. Corcoran and D. Levin, Gottlob Frege: Conceptual notation and related articles, Oxford University Press (1972), doi:10.1086/288549 |
| [125] | Fuchs, L.: Abelian Groups. Springer. Berlin (2015). doi:10.1007/978-3-319-19422-6 · Zbl 1416.20001 |
| [126] | Gaitsgory, D., Lurie, J.: Weil’s conjecture for function fields (2014-2017), [www.math.ias.edu/\( \sim\) lurie/papers/tamagawa-abridged.pdf] · Zbl 1439.14006 |
| [127] | Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures, in: Theorem Proving in Higher Order Logics. TPHOLs 2009, Lecture Notes in Computer Science 5674 Springer, Berlin (2009), doi:10.1007/978-3-642-03359-9_23 |
| [128] | Gawedzki, K., Conformal field theory: a case study, in Conformal Field Theory-New Non-perturbative Methods in String and Field Theory, CRC Press, 2000 · doi:10.1201/9780429502873 |
| [129] | Gell-Mann, M., The interpretation of the new particles as displaced charge multiplets, Nuovo Cim, 4, 2, 848-866, 1956 · doi:10.1007/BF02748000 |
| [130] | Gentzen, G., Untersuchungen über das logische Schließen, Math. Zeitschrift, 39, 176-210, 1935 · JFM 60.0020.02 · doi:10.1007/BF01201353 |
| [131] | Gentzen, G.: Investigations into Logical Deduction, translated by M. E. Szabo (ed.) in: The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics 55, Springer, Berlin (1969), 68-131, [ISBN:9780444534194] |
| [132] | Geuvers, H.; Niqui, M.; Spitters, B.; Wiedijk, F., Constructive analysis, types and exact real numbers, Math. Struc. Comput. Sci., 17, 1, 3-36, 2007 · Zbl 1157.03036 · doi:10.1017/S0960129506005834 |
| [133] | Goerss, P., Jardine, J.F.: Simplicial Homotopy Theory, Progress in Mathematics. Birkhäuser. Boston (2009). doi:10.1007/978-3-0346-0189-4 · Zbl 1195.55001 |
| [134] | Götz, L.: Martin-Löf’s J-rule, Bachelor’s Thesis, Ludwig Maximili an Univ., Munich, 2018, [math.lmu.de/\( \sim\) petrakis/Goetz.pdf] |
| [135] | Golze, D.; Icker, M.; Berger, S., Implementation of two-qubit and three-qubit quantum computers using liquid-state nuclear magnetic resonance, Concepts Mag. Resonance, 40A, 1, 25-37, 2012 · doi:10.1002/cmr.a.21222 |
| [136] | Govzmann, A., Pištalo, D., Poncin, N.: Indeterminacies and models of homotopy limits, [arXiv:2109.12395] · Zbl 07823985 |
| [137] | Grady, D., Sati, H.: Twisted differential \({{\rm KO}} \)-theory, [arXiv:1905.09085] · Zbl 1476.19007 |
| [138] | Grant, E.K., Humble, T.S.: Adiabatic Quantum Computing and Quantum Annealing. Oxford Research Encyclopedia (2020). doi:10.1093/acrefore/9780190871994.013.32 |
| [139] | Griffiths, PA, Periods of integrals on algebraic manifolds: summary of main results and discussion of open problems, Bull. Am. Math. Soc., 76, 228-296, 1970 · Zbl 0214.19802 · doi:10.1090/S0002-9904-1970-12444-2 |
| [140] | Grothendieck, A.: On the de Rham cohomology of algebraic varieties, Inst. Hautes Études Sci. Publ. Math. 29 (1966), 95-103 · Zbl 0145.17602 |
| [141] | Gu, X.; Haghighat, B.; Liu, Y., Ising- and Fibonacci-Anyons from KZ-equations, J. High Energy Phys., 2022, 15, 2022 · Zbl 1531.81276 · doi:10.1007/JHEP09(2022)015 |
| [142] | Gunter, C.A.: The Semantics of Types in Programming Languages, in: Handbook of Logic in Computer Science, Vol 3: Semantic structures, Oxford University Press (1995), [ISBN:9780198537625] |
| [143] | Hardie, KA; Kamps, KH; Kieboom, R., A homotopy bigroupoid of a topological space, Appl. Categ. Struct., 9, 311-327, 2001 · Zbl 0987.18006 · doi:10.1023/A:1011270417127 |
| [144] | Harper, R.: Practical Foundations for Programming Languages, Cambridge University Press (2016), [ISBN:9781107150300] · Zbl 1347.68001 |
| [145] | Hartnoll, S., Lucas, A., Sachdev, S.: Holographic quantum matter, MIT Press, Boston, (2018), [ISBN:9780262348010], [arXiv:1612.07324] · Zbl 1407.82005 |
| [146] | Hatcher, A.: Algebraic Topology, Cambridge University Press (2002) [ISBN:9780521795401], [https://pi.math.cornell.edu/ hatcher/AT/ATpage.html] · Zbl 1044.55001 |
| [147] | Hilton, P., Subjective history of homology and homotopy theory, Math. Mag., 61, 5, 282-291, 1988 · Zbl 0684.55001 · doi:10.2307/2689545 |
| [148] | Hofmann, M.: Extensional concepts in intensional type theory, Ph.D. thesis, Edinburgh (1995), Distinguished Dissertations, Springer (1997), [ECS-LFCS-95-327],doi:10.1007/978-1-4471-0963-1 |
| [149] | Hofmann, M.: Syntax and semantics of dependent types, in: Semantics and logics of computation, Publ. Newton Inst. 14, Cambridge University Press (1997), pp. 79-130, doi:10.1017/CBO9780511526619.004 · Zbl 0919.68083 |
| [150] | Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-five years of constructive type theory, Oxf. Logic Guides. 36, Clarendon Press (1998), pp. 83-111, [ISBN:9780198501275] · Zbl 0930.03089 |
| [151] | Hormozi, L.; Bonesteel, NE; Simon, SH, Topological quantum computing with Read-Rezayi states, Phys. Rev. Lett., 103, 160501, 2009 · doi:10.1103/PhysRevLett.103.160501 |
| [152] | Hormozi, L.; Zikos, G.; Bonesteel, NE; Simon, SH, Topological quantum compiling, Phys. Rev. B, 75, 165310, 2007 · doi:10.1103/PhysRevB.75.165310 |
| [153] | Hou, K.-B., Finster, E., Licata, D., Lumsdaine, P.: A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016), pp. 565-574, doi:10.1145/2933575.2934545, [arXiv:1605.03227] · Zbl 1395.55011 |
| [154] | Huang, H-L; Wu, D.; Fan, D.; Zhu, X., Superconducting quantum computing: a review, Sci. China Inf. Sci., 63, 8, 1-32, 2020 · doi:10.1007/s11432-020-2881-9 |
| [155] | Jacobs, B., Comprehension categories and the semantics of type dependency, Theor. Comput. Sci., 107, 2, 169-207, 1993 · Zbl 0804.18007 · doi:10.1016/0304-3975(93)90169-T |
| [156] | Jacobs, B.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998), [ISBN:9780444501707] · Zbl 0911.03001 |
| [157] | James, I.M.: General Topology and Homotopy Theory. Springer. Berlin (1984). doi:10.1007/978-1-4613-8283-6 · Zbl 0562.54001 |
| [158] | Jänich, K.: Topology, Undergraduate Texts in Mathematics, Springer, Berlin (1984), [ISBN:9780387908922] · Zbl 0567.54001 |
| [159] | Johansen, EG; Simula, T., Fibonacci anyons versus Majorana fermions-A Monte Carlo Approach to the Compilation of Braid Circuits in \({{\rm SU}}(2)_k\) Anyon Models, PRX Quantum, 2, 010334, 2021 · doi:10.1103/PRXQuantum.2.010334 |
| [160] | Johnson, DL, Presentations of Groups, 1990, Cambridge: Cambridge University Press, Cambridge · Zbl 0696.20027 |
| [161] | Joyal, A.: Notes on Clans and Tribes, [arXiv:1710.10238] |
| [162] | Jurčo, B.; Saemann, C.; Schreiber, U.; Wolf, M., Higher structures in M-theory, Fortsch. Phys., 67, 8-9, 2019 · Zbl 1535.81201 |
| [163] | Kachapova, F.: Formalizing groups in type theory, [arXiv:2102.09125] · Zbl 1347.03104 |
| [164] | Kadowaki, T.; Nishimori, H., Quantum annealing in the transverse Ising model, Phys. Rev. E, 58, 5355-5363, 1998 · doi:10.1103/PhysRevE.58.5355 |
| [165] | Kamps, KH; Porter, T., Abstract Homotopy and Simple Homotopy Theory, 1997, Singapore: World Scientific, Singapore · Zbl 0890.55014 · doi:10.1142/2215 |
| [166] | Kapulkin, C., LeFanu Lumsdaine, P., Voevodsky, V.: Univalence in simplicial sets, [arXiv:1203.2553] · Zbl 1452.03038 |
| [167] | Kapulkin, C.; LeFanu Lumsdaine, P., The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc., 23, 2071-2126, 2021 · Zbl 1471.18025 · doi:10.4171/jems/1050 |
| [168] | Katz, NM, On the differential equations satisfied by period matrices, Inst. Hautes Études Sci. Publ. Math., 35, 223-258, 1968 · Zbl 0159.22502 · doi:10.1007/BF02698924 |
| [169] | Katz, NM; Oda, T., On the differentiation of de Rham cohomology classes with respect to parameters, J. Math. Kyoto Univ., 8, 199-213, 1968 · Zbl 0165.54802 · doi:10.1215/kjm/1250524135 |
| [170] | Kauffman, LH; Lomonaco, SJ Jr, Braiding operators are universal quantum gates, New J. Phys., 6, 134, 2004 · doi:10.1088/1367-2630/6/1/134 |
| [171] | Kitaev, A., Quantum computations: algorithms and error correction, Russian Math. Surv., 52, 1191-1249, 1997 · Zbl 0917.68063 · doi:10.1070/rm1997v052n06abeh002155 |
| [172] | Kitaev, A., Unpaired Majorana fermions in quantum wires, Phys. Usp., 44, 131, 131-136, 2001 · doi:10.1070/1063-7869/44/10S/S29 |
| [173] | Kitaev, A., Fault-tolerant quantum computation by anyons, Ann. Phys., 303, 2-30, 2003 · Zbl 1012.81006 · doi:10.1016/S0003-4916(02)00018-0 |
| [174] | Kitaev, A., Anyons in an exactly solved model and beyond, Ann. Phys., 321, 1, 2-111, 2006 · Zbl 1125.82009 · doi:10.1016/j.aop.2005.10.005 |
| [175] | Kitaev, A., Periodic table for topological insulators and superconductors, AIP Conf. Proc., 1134, 22, 2009 · Zbl 1180.82221 · doi:10.1063/1.3149495 |
| [176] | Kliuchnikov, V.; Bocharov, A.; Svore, KM, Asymptotically optimal topological quantum compiling, Phys. Rev. Lett., 112, 2014 · doi:10.1103/PhysRevLett.112.140504 |
| [177] | Knapp, A., Basic Algebra, 2006, Berlin: Springer, Berlin · Zbl 1106.00001 · doi:10.1007/978-0-8176-4529-8 |
| [178] | Knill, E.: Conventions for quantum pseudocode, Los Alamos Technical Report LA-UR-96-2724 (1996), doi:10.2172/366453 |
| [179] | Kochen, S., Ultraproducts in the theory of models, Ann. Math., 74, 2, 221-261, 1961 · Zbl 0132.24602 · doi:10.2307/1970235 |
| [180] | Kohno, T.: Conformal field theory and topology, Transl Math. Monogr. 210, Amer. Math. Soc., Providence, RI (2002), [ams:mmono-210] · Zbl 1024.81001 |
| [181] | Kohno, T., Homological representations of braid groups and KZ connections, J. Singularities, 5, 94-108, 2012 · Zbl 1292.32019 · doi:10.5427/jsing.2012.5g |
| [182] | Kolganov, N.; Mironov, S.; Morozov, A., Large \(k\) topological quantum computer, Nucl. Phys. B, 987, 2023 · Zbl 1520.81038 · doi:10.1016/j.nuclphysb.2023.116072 |
| [183] | Kolmogorov, A., Zur Deutung der intuitionistischen Logik, Math. Z., 35, 58-65, 1932 · Zbl 0004.00201 · doi:10.1007/BF01186549 |
| [184] | Kraus, N.: The General Universal Property of the Propositional Truncation. In: TYPES 2014, Leibniz International Proceedings in Informatics (LIPIcs) 39 (2015) [arXiv:1411.2682] doi:10.4230/LIPIcs.TYPES.2014.111 · Zbl 1434.03150 |
| [185] | Krebbers, R.; Spitters, B., Type classes for efficient exact real arithmetic in Coq, Logical Methods Comput. Sci., 9, 1, 958, 2013 · doi:10.2168/LMCS-9(1:1)2013 |
| [186] | Krömer, R., Tool and Object: A History and Philosophy of Category Theory, 2007, Berlin: Springer, Berlin · Zbl 1114.18001 · doi:10.1007/978-3-7643-7524-9 |
| [187] | Ladyman, J.; Presnell, S., Identity in homotopy type theory, part I: the justification of path induction, Philos. Math., 23, 3, 386-406, 2015 · Zbl 1380.03027 · doi:10.1093/philmat/nkv014 |
| [188] | Lawvere, W.: Quantifiers and sheaves, Actes Congrès intern. Math. 1 (1970), 329-334, [ncatlab.org/nlab/files/Lawvere-QuantifiersAndSheaves.pdf] · Zbl 0261.18010 |
| [189] | Lawvere, W., Cohesive Toposes and Cantor’s “lauter Einsen.”, Philos. Math., 2, 1, 5-15, 1994 · Zbl 0801.18005 · doi:10.1093/philmat/2.1.5 |
| [190] | Lawvere, W., Axiomatic cohesion, Theory, 19, 3, 41-49, 2007 · Zbl 1123.18001 |
| [191] | Lee, E.-K.: A positive presentation of the pure braid group, J. Chungcheong Math. Soc. 23(3), 555-561, (2010), [JAKO201007648745187] |
| [192] | van Leeuwen, J.: Wiedermann: Knowledge, Representation and the Dynamics of Computation, Studies in Applied Philosophy, vol. 28, pp. 69-89. Springer, Berlin (2017). doi:10.1007/978-3-319-43784-2_5 |
| [193] | Leinaas, JM; Myrheim, J., On the theory of identical particles, Nuovo Cim B, 37, 1-23, 1977 · doi:10.1007/BF02727953 |
| [194] | Lerda, A.: Anyons - Quantum Mechanics of Particles with Fractional Statistics, Lect. Notes Phys. 14, Springer, Berlin (1992), doi:10.1007/978-3-540-47466-1 · Zbl 0785.60048 |
| [195] | Lewis, C.I.: A Survey of Symbolic Logic, Univ. of California Press, Berkeley, (1918), [archive.org/details/surveyofsymbolic00lewiiala] |
| [196] | Leymann, F.; Barzen, J., The bitter truth about gate-based quantum algorithms in the NISQ era, Quant. Sci. Technol., 5, 2020 · doi:10.1088/2058-9565/abae7d |
| [197] | Li, N.: Quotient Types in Type Theory, PhD Thesis, Nottingham (2014), [eprints.nottingham.ac.uk:28941], [ncatlab.org/nlab/files/Li-QuotientTypes.pdf] |
| [198] | Liao, A., Coates, J., Mullanix, R.: 1lab, [https://1lab.dev] |
| [199] | Licata, D., Finster, E.: Eilenberg-MacLane spaces in homotopy type theory, CSL-LICS ‘14 66, 1-9, (2014) doi:10.1145/2603088.2603153 · Zbl 1395.68249 |
| [200] | Lubarsky, R., On the cauchy completeness of the constructive cauchy reals, Electron. Notes Theor. Comput. Sci., 167, 225-254, 2007 · Zbl 1262.03126 · doi:10.1016/j.entcs.2006.09.012 |
| [201] | Lüders, G., Über die Zustandsänderung durch den Meßprozeß, Ann. Phys., 8, 322-328, 1951 · Zbl 0043.21003 |
| [202] | Lundfall, M.: Formalizing real numbers in Agda, preprint (2015), [ncatlab.org/nlab/files/Lundfall-RealNumbersInAgda.pdf] |
| [203] | Luo, Z.: Computation and Reasoning-A Type Theory for Computer Science, Clarendon Press, Oxford (1994), [ISBN:9780198538356] · Zbl 0823.68101 |
| [204] | Lurie, J.: Higher Topos Theory, Ann. Math. Stud. 170, Princeton University Press (2009), [pup:8957], [arXiv:math/0608040] · Zbl 1175.18001 |
| [205] | Lurie, J.: Higher Algebra, [https://www.math.ias.edu/\( \sim\) lurie/papers/HA.pdf] · Zbl 1175.18001 |
| [206] | Macaluso, E.; Comparin, T.; Mazza, L.; Carusotto, I., Fusion channels of non-abelian anyons from angular-momentum and density-profile measurements, Phys. Rev. Lett., 123, 2019 · doi:10.1103/PhysRevLett.123.266801 |
| [207] | Magnus, W., Karras, A., Solitar, D.: Combinatorial group theory: presentation of groups in terms of generators and relations, Dover Publications (2004), [ISBN-13:9780486438306] · Zbl 1130.20307 |
| [208] | Manin, Y.I.: Algebraic curves over fields with differentiation (Russian), Izv. Akad. Nauk SSSR. Ser. Mast. 22 (1958), 737-756, [bookstore.ams.org/trans2-37], [books.google.com/books?id=fZ7ms3db_cMC] · Zbl 0151.27503 |
| [209] | Manin, Y.I.: Computable and Uncomputable, Sov. Radio (1980), published in: Mathematics as Metaphor: Selected essays of Yuri I. Manin, Collected Works 20, AMS (2007), 69-77, [ISBN:978-0-8218-4331-4] |
| [210] | Manin, Y.I.: Classical computing, quantum computing, and Shor’s factoring algorithm, Séminaire Bourbaki exp. 862, Astérisque 266 (2000), 375-404 · Zbl 1005.81014 |
| [211] | Marra, P., Majorana nanowires for topological quantum computation: a tutorial, J. Appl. Phys., 132, 2022 · doi:10.1063/5.0102999 |
| [212] | Martin-Löf, P.: A Theory of Types, unpublished note (1971), [ncatlab.org/nlab/files/MartinLoef1971-ATheoryOfTypes.pdf] · Zbl 0231.02039 |
| [213] | Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Logic Colloquium ‘73, Studies in Logic and the Foundations of Mathematics 80, 73-118, (1975) · Zbl 0334.02016 |
| [214] | Martin-Löf, P., Constructive mathematics and computer programming, Stud. Logic Found. Math., 104, 153-175, 1982 · Zbl 0541.03034 · doi:10.1016/S0049-237X(09)70189-2 |
| [215] | Martin-Löf, P.: (notes by G. Sambin of a series of lectures given in Padua in 1980), Intuitionistic type theory, Bibliopolis, Naples (1984), [ncatlab.org/nlab/files/MartinLofIntuitionisticTypeTheory.pdf] · Zbl 0571.03030 |
| [216] | Martin-Löf, P.: On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic J. Philosophical Logic 1 (1996), 11-60, [docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf] · Zbl 0885.03009 |
| [217] | Masaki, Y., Mizushima, T., Nitta, M.: Non-Abelian Anyons and Non-Abelian Vortices in Topological Superconductors, [arXiv:2301.11614] |
| [218] | Mashayekhy, B., Mirebrahimi, H.: Some Properties of Finitely Presented Groups with Topological Viewpoints, Int. J. Math., Game Theory, and Algebra 18(6), 511-515, (2010), [arXiv:1012.1744] · Zbl 1211.57001 |
| [219] | Matekole, E.S., Fang, Y.-L L., Lin, M.: Methods and Results for Quantum Optimal Pulse Control on Superconducting Qubit Systems, 2022 IEEE International Parallel and Distributed Processing Symposium Workshops (2022), doi:10.1109/IPDPSW55747.2022.00102, [arXiv:2202.03260] |
| [220] | Mawson, T.; Petersen, T.; Slingerland, J.; Simula, T., Braiding and fusion of non-Abelian vortex anyons, Phys. Rev. Lett., 123, 2019 · doi:10.1103/PhysRevLett.123.140404 |
| [221] | May, P.: The Geometry of Iterated Loop Spaces. Springer, Berlin (1972). doi:10.1007/BFb0067491 · Zbl 0244.55009 |
| [222] | May, P., Infinite loop space theory, Bull. Am. Math. Soc., 83, 4, 456-494, 1977 · Zbl 0357.55016 · doi:10.1090/S0002-9904-1977-14318-8 |
| [223] | May, P., Sigurdsson, J.: Parametrized Homotopy Theory, Math. Surv. Monogr. 132 Amer. Math. Soc. (2006), [ISBN:9781470413590], [arXiv:math/0411656] · Zbl 1119.55001 |
| [224] | Miller, W.: Symmetry Groups and Their Applications, Pure and Applied Mathematics 50, pp. 16-60, Elsevier, (1972) [ISBN:9780080873657] · Zbl 0306.22001 |
| [225] | Miller, H. (ed.): Handbook of Homotopy Theory, Chapman and Hall/CRC Press (2019), [ISBN:9780815369707], doi:10.1201/9781351251624 |
| [226] | Milne, J.: Étale Cohomology, Mathematical Series 33, Princeton University Press (1980), [ISBN:9780691082387], [jstor:j.ctt1bpmbk1] · Zbl 0433.14012 |
| [227] | Mochon, C., Anyons from non-solvable finite groups are sufficient for universal quantum computation, Phys. Rev. A, 67, 2003 · doi:10.1103/PhysRevA.67.022315 |
| [228] | Mochon, C., Anyon computers with smaller groups, Phys. Rev. A, 69, 2004 · doi:10.1103/PhysRevA.69.032306 |
| [229] | Møller, J.: The fundamental group and covering spaces, lecture notes, [arXiv:1106.5650] |
| [230] | Munkres, J.: Topology, Pearson (2013), [ISBN:1292023627] |
| [231] | Muro, F.: Representability of Cohomology Theories, talk at Joint Math. Conf, CSASC, Prague (2010), [ncatlab.org/nlab/files/Muro-Representability.pdf] |
| [232] | Murray, Z.: Constructive Analysis in the Agda Proof Assistant, [arXiv:2205.08354], [github.com/z-murray/honours-project-constructive-analysis-in-agda] |
| [233] | Myers, D.J.: Modal Fracture of Higher Groups, Diff. Geom. Appl. (2024, in print) [arXiv:2106.15390] |
| [234] | Myers, D.J.: Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory, [arXiv:2205.15887] |
| [235] | Myers, D.J., Riley, M.: Commuting cohesions, [arXiv:2301.13780] |
| [236] | Nayak, C.; Simon, SH; Stern, A.; Freedman, M.; Das Sarma, S., Non-abelian anyons and topological quantum computation, Rev. Mod. Phys., 80, 1083-1159, 2008 · Zbl 1205.81062 · doi:10.1103/RevModPhys.80.1083 |
| [237] | Nenciu, G., On the adiabatic theorem of quantum mechanics, J. Phys. A: Math. Gen., 13, L15, 1980 · Zbl 0435.47025 · doi:10.1088/0305-4470/13/2/002 |
| [238] | Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information, Cambridge University Press, (2010), [ISBN:9780511976667] · Zbl 1288.81001 |
| [239] | Nielsen, MA; Dowling, MR; Gu, M.; Doherty, AC, Quantum computation as geometry, Science, 311, 5764, 1133-1135, 2006 · Zbl 1226.81049 · doi:10.1126/science.1121541 |
| [240] | Nikolaus, T.; Schreiber, U.; Stevenson, D., Principal \(\infty \)-bundles - General theory, J. Homotopy Rel. Struc., 10, 749-801, 2015 · Zbl 1349.18032 · doi:10.1007/s40062-014-0083-6 |
| [241] | Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990), [www.cse.chalmers.se/research/group/logic/book] · Zbl 0744.03029 |
| [242] | Norell, U., Dependently typed programming in Agda, in advanced functional programming AFP 2008, Lect. Notes Comput. Sci., 5832, 230-266, 2009 · Zbl 1263.68038 · doi:10.1007/978-3-642-04652-0_5 |
| [243] | Ogburn, R.W., Preskill, J.: Topological Quantum Computation, In: Williams, C.P. (Ed.), Quantum Computing and Quantum Communications, Lect. Notes Comput. Sci. 1509, 341, Springer, Berlin (1999), doi:10.1007/3-540-49208-9-31 · Zbl 0960.81009 |
| [244] | Pachos, JK, Introduction to Topological Quantum Computation, 2012, Cambridge: Cambridge University Press, Cambridge · Zbl 1247.81003 · doi:10.1017/CBO9780511792908 |
| [245] | Palmgren, E.: On Universes in Type Theory. In: Twenty-Five Years of Constructive Type Theory, Oxford University Press (1998), 191-204, doi:10.1093/oso/9780198501275.003.0012 · Zbl 0930.03090 |
| [246] | Paulin-Mohring, C.: Inductive definitions in the system Coq-Rules and Properties. In: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993), doi:10.1007/BFb0037116 · Zbl 0844.68073 |
| [247] | Pavlović, D.: Categorical interpolation: Descent and the Beck-Chevalley condition without direct images, In: Category Theory, Lecture Notes in Mathematics 1488, Springer, Berlin (1991), doi:10.1007/BFb0084229, [isg.rhul.ac.uk/dusko/papers/1990-BCDE-Como.pdf] · Zbl 0736.18005 |
| [248] | Polyakov, A., String theory and quark confinement, Nucl. Phys. Proc. Suppl., 68, 1-8, 1998 · Zbl 0999.81527 · doi:10.1016/S0920-5632(98)00135-2 |
| [249] | Polyakov, A., The wall of the cave, Int. J. Mod. Phys. A, 14, 645-658, 1999 · Zbl 0931.81013 · doi:10.1142/S0217751X99000324 |
| [250] | Polyakov, A.: Gauge Fields and Space-Time, Int. J. Mod. Phys. A 17 S1 (2002), 119-136, doi:10.1142/S0217751X02013071. [arXiv:hep-th/0110196], · Zbl 1025.83032 |
| [251] | Potts, P., Edalat, A.: Exact real computer arithmetic, preprint (1997), [ncatlab.org/nlab/files/PottsEdalat-ExactRealComputerArithmetic.pdf] · Zbl 0911.68108 |
| [252] | Preskill, J., Quantum computing in the NISQ era and beyond, Quantum, 2, 79, 2018 · doi:10.22331/q-2018-08-06-79 |
| [253] | Preskill, J.: The Physics of Quantum Information, talk at The Physics of Quantum Information, 28th Solvay Conference on Physics (2022), [arXiv:2208.08064] |
| [254] | Quillen, D.: Homotopical Algebra, Lecture Notes in Mathematics 43 Springer, (1967), doi:10.1007/BFb0097438 · Zbl 0168.20903 |
| [255] | Rajak, A.; Suzuki, S.; Dutta, A.; Chakrabarti, BK, Quantum annealing: an overview, Phil. Trans. R. Soc. A, 381, 20210417, 2022 · doi:10.1098/rsta.2021.0417 |
| [256] | Rao, S.: Introduction to abelian and non-abelian anyons, In: Topology and Condensed Matter Phys. Texts & Read. 19 Springer (2017), 399-437, doi:10.1007/978-981-10-6841-6_16, [arXiv:1610.09260] · Zbl 1390.81550 |
| [257] | Renes, JM, Quantum Information Theory, 2022, Basel: De Gruyter, Basel · Zbl 1492.81005 · doi:10.1515/9783110570250 |
| [258] | Rezk, C.: Toposes and homotopy toposes, lecture notes (2010), [ncatlab.org/nlab/files/Rezk_HomotopyToposes.pdf] |
| [259] | Rho, M., Zahed, I. (eds.): The Multifaceted Skyrmion, World Scientific, Singapore (2016), doi:10.1142/9710 |
| [260] | Richter, B., From Categories to Homotopy Theory, 2020, Cambridge: Cambridge University Press, Cambridge · Zbl 1465.18001 · doi:10.1017/9781108855891 |
| [261] | Rieffel, E.; Polak, W., Quantum Computing-A Gentle Introduction, 2011, Boston: MIT Press, Boston · Zbl 1221.81003 |
| [262] | Riehl, E.: Categorical Homotopy Theory, Cambridge University Press (2014), [ISBN:9781107048454] · Zbl 1317.18001 |
| [263] | Riehl, E.: On the \(\infty \)-topos semantics of homotopy type theory, lecture at Logic and higher structures, CIRM (2022), [emilyriehl.github.io/files/semantics.pdf] |
| [264] | Rigolin, G.; Ortiz, G., The adiabatic theorem for quantum systems with spectral degeneracy, Phys. Rev. A, 85, 2012 · doi:10.1103/PhysRevA.85.062111 |
| [265] | Rijke, E.: Introduction to Homotopy Type Theory, lecture at CMU (2018) [www.andrew.cmu.edu/user/erijke/hott] [ncatlab.org/nlab/files/Rijke-IntroductionHoTT-2018.pdf] |
| [266] | Rijke, E.: Classifying Types, PhD Thesis, Carnegie Mellon University, [arXiv:1906.09435] |
| [267] | Rijke, E.: Introduction to Homotopy Type Theory, Cambridge University Press (in print), [arXiv:2212.11082] · Zbl 1362.03007 |
| [268] | Rijke, E., Shulman, M., Spitters, B.: Modalities in Homotopy Type Theory, 16 (2020) 1, doi:10.23638/LMCS-16(1:2)2020, [arXiv:1706.07526] · Zbl 1489.03005 |
| [269] | Rijke, E.; Spitters, B., Sets in homotopy type theory, Math. Struct. Comput. Sci., 25, 5, 1172-1202, 2015 · Zbl 1362.03007 · doi:10.1017/S0960129514000553 |
| [270] | Riley, M.: A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis, Wesleyan University, (2022), doi:10.14418/wes01.3.139 |
| [271] | Ringer, T., Porter, R., Yazdani, N., Leo, J., Grossman, D.: Proof Repair across Type Equivalences, [arXiv:2010.00774] |
| [272] | Roberts, C.D.: Origin of the Proton Mass, [arXiv:2211.09905] |
| [273] | Roberts, CD, On Mass and Matter, AAPPS Bull., 31, 6, 2021 · doi:10.1007/s43673-021-00005-4 |
| [274] | Roberts, CD; Schmidt, SM, Reflections upon the emergence of hadronic mass, Eur. Phys. J. Special Top., 229, 3319-3340, 2020 · doi:10.1140/epjst/e2020-000064-6 |
| [275] | Rotman, JJ, An Introduction to the Theory of Groups, 1995, Berlin: Springer, Berlin · Zbl 0810.20001 · doi:10.1007/978-1-4612-4176-8 |
| [276] | Rotman, JJ, An Introduction to Algebraic Topology, 1988, Berlin: Springer, Berlin · Zbl 0661.55001 · doi:10.1007/978-1-4612-4576-6 |
| [277] | Rowell, E.: Braids, Motions and Topological Quantum Computing, [arXiv:2208.11762] |
| [278] | Rowell, EC; Wang, Z., Mathematics of Topological Quantum Computing, Bull. Am. Math. Soc., 55, 183-238, 2018 · Zbl 1437.81005 · doi:10.1090/bull/1605 |
| [279] | Rudin, W.: Principles of Mathematical Analysis, McGraw-Hill (1976), [ISBN13:9780070542358] · Zbl 0346.26002 |
| [280] | Rudolph, G., Schmidt, M.: Differential Geometry and Mathematical Physics - Part II. Fibre Bundles, Topology and Gauge Fields, Springer, Berlin (2017), doi:10.1007/978-94-024-0959-8 · Zbl 1364.53001 |
| [281] | Russell, B., Whitehead, A.: Principia Mathematica, Cambridge University Press (1910, 1927), [ISBN:9780521067911] · JFM 41.0083.02 |
| [282] | Sakaguchi, K.: Validating Mathematical Structures, in: Automated Reasoning. IJCAR 2020, Lecture Notes in Computer Science 12167 Springer (2020), doi:10.1007/978-3-030-51054-1_8 · Zbl 07614666 |
| [283] | Santini, A.: Topological groupoids, Kandidatproject, Copenhagen University (2011), [ncatlab.org/nlab/files/Santini-Groupoids.pdf] |
| [284] | Sati, H.: M-theory and matter via twisted equivariant differential (TED) K-theory, talk at M-Theory and Mathematics 2023, CQTS @ NYU Abu Dhabi (2023) |
| [285] | Sati, H., Schreiber, U.: Differential Cohomotopy implies intersecting brane observables via configuration spaces and chord diagrams, Adv. Theor. Math. Physics 26 (2022) 4, [ISSN:1095-0753], [arXiv:1912.10425] · Zbl 1520.83100 |
| [286] | Sati, H.; Schreiber, U., Equivariant Cohomotopy implies orientifold tadpole cancellation, J. Geom. Phys., 156, 2020 · Zbl 1450.81055 · doi:10.1016/j.geomphys.2020.103775 |
| [287] | Sati, H., Schreiber, U.: Proper Orbifold Cohomology, [arXiv:2008.01101] |
| [288] | Sati, H., Schreiber, U.: M/F-Theory as \(M\!f\)-Theory, Rev. Math. Phys. 35 10 (2023) [arXiv:2103.01877] doi:10.1142/S0129055X23500289 · Zbl 1538.81049 |
| [289] | Sati, H., Schreiber, U.: Equivariant principal \(\infty \)-bundles, [arXiv:2112.13654] · Zbl 1450.81055 |
| [290] | Sati, H.; Schreiber, U., Anyonic defect branes in TED-K-theory, Rev. Math. Phys., 2023 · Zbl 1539.81108 · doi:10.1142/S0129055X23500095 |
| [291] | Sati, H.; Schreiber, U., Anyonic topological order in TED-K-theory, Rev. Math. Phys., 35, 3, 2350001, 2023 · Zbl 1521.19003 · doi:10.1142/S0129055X23500010 |
| [292] | Sati, H., Schreiber, U.: Topological Quantum Programming in TED-K, PlanQC 2022 33 (2022), [arXiv:2209.08331], [ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K] · Zbl 1521.19003 |
| [293] | Sati, H., Schreiber, U.: Entanglement of Sections: The pushout of entangled and parameterized quantum information [arXiv:2309.07245] |
| [294] | Sati, H., Schreiber, U.: The Quantum Monadology, [arXiv:2310.15735] |
| [295] | Sati, H.; Schreiber, U.; Stasheff, J., Twisted differential string and fivebrane structures, Commun. Math. Phys., 315, 169-213, 2012 · Zbl 1252.81110 · doi:10.1007/s00220-012-1510-3 |
| [296] | Sau, J.: A Roadmap for a Scalable Topological Quantum Computer, Physics 10 (2017) 68, [physics.aps.org/articles/v10/68] |
| [297] | Schreiber, U.: Differential cohomology in a cohesive \(\infty \)-topos, Habilitation thesis, [arXiv:1310.7930] |
| [298] | Schreiber, U.: Quantization via Linear Homotopy Types, talk notes, Paris Diderot and ESI Vienna (2014), [arXiv:1402.7041] |
| [299] | Schreiber, U.: Differential generalized cohomology in Cohesive homotopy type theory, talk at Formalization of Mathematics, Inst. H. Poincaré, Paris (May 2014), [ncatlab.org/schreiber/files/SchreiberParis2014.pdf] |
| [300] | Schreiber, U.: Some thoughts on the future of modal homotopy type theory, talk at German Mathematical Society meeting, Hamburg (Sept 2015), [ncatlab.org/schreiber/files/SchreiberDMV2015b.pdf] |
| [301] | Schreiber, U.: Knots for quantum computation from defect branes, talk at Workshop on Topological Methods in Mathematical Physics, Erice (Sep 2022), [ncatlab.org/schreiber/show/Knots+for+quantum+computation+from+defect+branes] |
| [302] | Schreiber, U.: Quantum types via Linear Homotopy Type Theory, talk at Workshop on Quantum Software @ QTML2022, Naples (Nov 2022), [ncatlab.org/schreiber/files/QuantumDataInLHoTT-221117.pdf] |
| [303] | Schreiber, U.: Topological Quantum Gates from M-Theory, talk at M-Theory and Mathematics 2023, CQTS @ NYU Abu Dhabi (2023) |
| [304] | Schreiber, U.; Shulman, M., Quantum Gauge field theory in cohesive homotopy type theory, EPTCS, 158, 109-126, 2014 · Zbl 1464.81043 · doi:10.4204/EPTCS.158.8 |
| [305] | Schubert, H., Categories, 1972, Berlin: Springer, Berlin · Zbl 0253.18002 · doi:10.1007/978-3-642-65364-3 |
| [306] | Schwarz, J.: The Second Superstring Revolution, lecture at Sakharov Conference (Moscow, May 1996), [inspire:969846], [arXiv:hep-th/9607067] |
| [307] | Scott, D.S.: Outline of a mathematical theory of computation, in: Proc. 4th Ann. Princeton Conf. on Information Sciences and Systems (1970), 169-176, [ncatlab.org/nlab/files/Scott-TheoryOfComputation.pdf] |
| [308] | Scott, D.S., Strachey, C.: Toward a Mathematical Semantics for Computer Languages, Oxford Univ. Computing Laboratory, Technical Monograph PRG-6 (1971), [www.cs.ox.ac.uk/files/3228/PRG06.pdf] · Zbl 0268.68004 |
| [309] | Seely, RAG, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc., 95, 33-48, 1984 · Zbl 0539.03048 · doi:10.1017/S0305004100061284 |
| [310] | Segal, G., Configuration-spaces and iterated loop-spaces, Invent. Math., 21, 213-221, 1973 · Zbl 0267.55020 · doi:10.1007/BF01390197 |
| [311] | Selinger, P., Towards a quantum programming language, Math. Struct. Comput. Sci., 14, 527-586, 2004 · Zbl 1085.68014 · doi:10.1017/S0960129504004256 |
| [312] | Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings of 35th Annual Symposium on Foundations of Computer Science (1994), pp. 124-134, doi:10.1109/SFCS.1994.365700 |
| [313] | Shor, PW, Scheme for reducing decoherence in quantum computer memory, Phys. Rev. A, 52, R2493(R), 1995 · doi:10.1103/PhysRevA.52.R2493 |
| [314] | Shulman, M.: Minicourse on Homotopy Type Theory, University of Swansea (2012), [http://home.sandiego.edu/\( \sim\) shulman/hottminicourse2012] |
| [315] | Shulman, M., Univalence for inverse diagrams and homotopy canonicity, Math. Struct. Comput. Sci., 25, 5, 1203-1277, 2015 · Zbl 1362.03008 · doi:10.1017/S0960129514000565 |
| [316] | Shulman, M., Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Math. Struct. Comput. Sci., 28, 6, 856-941, 2018 · Zbl 1390.03014 · doi:10.1017/S0960129517000147 |
| [317] | Shulman, M.: All \((\infty ,1)\)-toposes have strict univalent universes, [arXiv:1904.07004] |
| [318] | Simon, B., Holonomy, the quantum adiabatic theorem, and Berry’s phase, Phys. Rev. Lett., 51, 2167-2170, 1983 · doi:10.1103/PhysRevLett.51.2167 |
| [319] | Simon, DR, On the power of quantum computation, SIAM J. Comput., 26, 5, 1997 · Zbl 0883.03024 · doi:10.1137/S0097539796298637 |
| [320] | Simon, S.H.: Topological Quantum, lecture notes and proto-book (2021), [www-thphys.physics.ox.ac.uk/people/SteveSimon/topological2021/TopoBook-Sep1-2021.pdf] |
| [321] | Simpson, C.: A Giraud-type characterization of the simplicial categories associated to closed model categories as \(\infty \)-pretopoi, [arXiv:math/9903167] |
| [322] | Slonneger, K., Kurtz, B.: Denotational semantics, Formal Syntax and Semantics of Programming Languages, Addison-Wesley (1995), [https://homepage.divms.uiowa.edu/ slonnegr/plf/Book/] · Zbl 0844.68016 |
| [323] | Solovay, R.: Lie Groups and Quantum Circuits, talk in: Mathematics Of Quantum Computation workshop, MSRI (2000), [msri.org/workshops/189/schedules/12826] |
| [324] | Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism, Studies in Logic 149, Elsevier (2006), [ISBN:9780444520777] · Zbl 1183.03004 |
| [325] | Spanier, E., Algebraic Topology, 1982, Berlin: Springer, Berlin · Zbl 0477.55001 |
| [326] | Stanescu, T.D.: Introduction to Topological Quantum Matter & Quantum Computation, CRC Press (2020), [ISBN:9780367574116] · Zbl 1375.81015 |
| [327] | Steenrod, N.: Homology With Local Coefficients, Ann. Math. Sec. Ser. 44 (1943), 610-627, [jstor:1969099] · Zbl 0061.40901 |
| [328] | Stern, A.; Lindner, NH, Topological quantum computation-from basic concepts to first experiments, Science, 339, 6124, 1179-1184, 2013 · doi:10.1126/science.1231473 |
| [329] | Streicher, T.: Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993), [ncatlab.org/nlab/files/Streicher-IntensionalTT.pdf] |
| [330] | Strocchi, F., An Introduction to Non-Perturbative Foundations of Quantum Field Theory, 2013, Oxford: Oxford University Press, Oxford · Zbl 1266.81002 · doi:10.1093/acprof:oso/9780199671571.001.0001 |
| [331] | Strom, J.: Modern Classical Homotopy Theory, Graduate Studies in Mathematics 127, Amer. Math. Soc., Providence, RI (2011), doi:10.1090/gsm/127 · Zbl 1231.55001 |
| [332] | Stump, A.: Verified Functional Programming in Agda. Association for Computing Machinery and Morgan & Claypool (2016). doi:10.1145/2841316 |
| [333] | Thompson, S.: Type Theory and Functional Programming, Addison-Wesley (1991), [ISBN:0201416670] · Zbl 0753.68026 |
| [334] | Todorov, I.; Hadjiivanov, L., Monodromy Representations of the Braid Group, Phys. Atom. Nucl., 64, 2059-2068, 2001 · doi:10.1134/1.1432899 |
| [335] | Toën, B.; Vezzosi, G., Homotopical algebraic geometry I: Topos theory, Adv. Math., 193, 2, 257-372, 2005 · Zbl 1120.14012 · doi:10.1016/j.aim.2004.05.004 |
| [336] | tom Dieck, T.: Transformation Groups, de Gruyter (1987), doi:10.1515/9783110858372 · Zbl 0611.57002 |
| [337] | tom Dieck, T.: Algebraic topology, Eur. Math. Soc. (2008), doi:10.4171/048 · Zbl 1156.55001 |
| [338] | Troelstra, A.S.: Principles of Intuitionism. Lecture Notes in Mathematics, vol. 95. Springer, Berlin (1969) · Zbl 0181.00504 |
| [339] | Troelstra, AS, Aspects of constructive mathematics, Stud. Logic Found. Math., 90, 973-1052, 1977 · doi:10.1016/S0049-237X(08)71127-3 |
| [340] | Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics - An introduction, Vol 1, Studies in Logic and the Foundations of Mathematics 121, North Holland (1988), [ISBN:9780444702661] · Zbl 0661.03047 |
| [341] | Tsementzis, D., Univalent foundations as structuralist foundations, Synthese, 194, 9, 3583-3617, 2017 · Zbl 1400.03023 · doi:10.1007/s11229-016-1109-x |
| [342] | UniMath, [unimath.github.io/UniMath], [unimath.github.io/agda-unimath] |
| [343] | Univalent Foundations Project, Homotopy Type Theory - Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013, [homotopytypetheory.org/book] · Zbl 1298.03002 |
| [344] | Valera, SJ, Fusion structure from exchange symmetry in \((2+1)\)-Dimensions, Ann. Phys., 429, 2021 · Zbl 1464.81060 · doi:10.1016/j.aop.2021.168471 |
| [345] | van den Berg, B.; Garner, R., Types are weak \(\omega \)-groupoids, Proc. London Math. Soc., 102, 2, 370-394, 2011 · Zbl 1229.18007 · doi:10.1112/plms/pdq026 |
| [346] | Vanderbilt, D., Berry Phases in Electronic Structure Theory-Electric Polarization, 2018, Cambridge: Orbital Magnetization and Topological Insulators. Cambridge University Press, Cambridge · Zbl 1401.82003 · doi:10.1017/9781316662205 |
| [347] | van Doorn, F.: On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, PhD dissertation, Carnegie Mellon (2018), [arXiv:1808.10690] |
| [348] | Veltri, N., van der Weide, N.: Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science 17 2 (2021), doi:10.23638/LMCS-17(2:8)2021, [arXiv:2002.08150] · Zbl 1498.03037 |
| [349] | Vezzosi, A., Mörtberg, A., Abel, A.: Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. In: Proceedings of the ACM on Programming Languages 3 ICFP 87 (2019), 1-29, doi:10.1145/3341691 · Zbl 1512.68058 |
| [350] | Voevodsky, V.: Univalent Foundations Project, grant proposal application (2010), [ncatlab.org/nlab/files/Voevodsky-UFP2010.pdf] |
| [351] | Voisin, C.: Hodge theory and Complex algebraic geometry I, translated by L. Schneps, Cambridge University Press (2002/3), doi:10.1017/CBO9780511615344 · Zbl 1005.14002 |
| [352] | Voisin, C.: Hodge theory and Complex algebraic geometry II, translated by L. Schneps, Cambridge University Press (2002/3), doi:10.1017/CBO9780511615177 · Zbl 1032.14001 |
| [353] | von Neumann, J.: Mathematische Grundlagen der Quantenmechanik, Springer (1932, 1971), doi:10.1007/978-3-642-96048-2; translated as: Mathematical Foundations of Quantum Mechanics Princeton University Press (1955), doi:10.1515/9781400889921 · JFM 58.0929.06 |
| [354] | Vuillemin, J.: Exact real computer arithmetic with continued fractions, in LFP ‘88: Proceedings of the 1988 ACM conference on LISP and functional programming (1988), pp. 14-27, doi:10.1145/62678.62681 |
| [355] | Wadler, P., Propositions as types, ACM Commun., 58, 12, 75-84, 2015 · doi:10.1145/2699407 |
| [356] | Wang, Z.: Topological Quantum Computation, CBMS Regional Conference Series in Mathematics 112 Amer. Math. Soc. (2010), [ISBN-13:978082184930-9] · Zbl 1239.81005 |
| [357] | Wärn, D.: Eilenberg-MacLane spaces and stabilisation in homotopy type theory, [arXiv:2301.03685] · Zbl 07752396 |
| [358] | Weinstein, A.: Groupoids: Unifying Internal and External Symmetry - A Tour through some Examples, Notices Amer. Math. Soc. 43 (1996), 744-752, [www.ams.org/notices/199607/weinstein.pdf] · Zbl 1044.20507 |
| [359] | Wellen, F.: Cartan Geometry in Modal Homotopy Type Theory, PhD Thesis, KIT (2017), [arXiv:1806.05966], [ncatlab.org/schreiber/show/thesis+Wellen] |
| [360] | Wen, X-G, Topological orders and Chern-Simons theory in strongly correlated quantum liquid, Int. J. Mod. Phys. B, 05, 10, 1641-1648, 1991 · doi:10.1142/S0217979291001541 |
| [361] | Wilczek, F.; Zee, A., Appearance of gauge structure in simple dynamical systems, Phys. Rev. Lett., 52, 24, 2111-2114, 1984 · doi:10.1103/PhysRevLett.52.2111 |
| [362] | Williams, L.: Configuration Spaces for the Working Undergraduate, Rose-Hulman Undergrad. Math. J. 21 (2020) 8, [rhumj:vol21/iss1/8], [arXiv:1911.11186] |
| [363] | Wilson, J.C.H.: The geometry and topology of braid groups, lecture at 2018 Summer School on Geometry and Topology, Chicago (2018), [ncatlab.org/nlab/files/Wilson-BraidGroups.pdf] |
| [364] | Yang, C.N., Ge, M.L. (eds.), Braid Group, Knot Theory and Statistical Mechanics, Adv. Ser. Mat. Phys. 9, World Scientific, Singapore (1991), doi:10.1142/0796 · Zbl 0716.00010 |
| [365] | Yap, C.-K., Dubé, T.: The exact computation paradigm. In: Computing in Euclidean Geometry, Lecture Notes Series on Computing, World Scientific (1995), 452-492, doi:10.1142/9789812831699_0011 |
| [366] | Zaanen, J.; Liu, Y.; Sun, Y-W; Schalm, K., Holographic Duality in Condensed Matter Physics, 2015, Cambridge: Cambridge University Press, Cambridge · doi:10.1017/CBO9781139942492 |
| [367] | Zanardi, P.; Rasetti, M., Holonomic quantum computation, Phys. Lett. A, 264, 94-99, 1999 · Zbl 0949.81009 · doi:10.1016/S0375-9601(99)00803-8 |
| [368] | Zucker, J.: Formalization of Classical Mathematics in Automath, Colloq. Internat. Cent. Nat. Rech. Scient. 249 (1975), 135-145, [www.win.tue.nl/automath/archive/webversion/aut042/aut042.html]; also in: Studies in Logic and the Foundations of Mathematics 133 (1994), 127-139, doi:10.1016/S0049-237X(08)70202-7 |
| [369] | Zulehner, A., Wille, R.: Simulation and Design of Quantum Circuits, in: Reversible Computation: Extending Horizons of Computing. RC 2020, Lecture Notes in Computer Science 12070, Springer, New York (2020), doi:10.1007/978-3-030-47361-7_3 · Zbl 1479.81004 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
