المؤلفون: Bordg, Anthony, Cavalleri, Nicolò

مصطلحات موضوعية: Computer Science - Logic in Computer Science, Mathematics - Differential Geometry, 03B35, 53-04

URL الوصول: http://arxiv.org/abs/2108.00484

المؤلفون: Bordg, Anthony, Paulson, Lawrence, Li, Wenda

المصدر: Experimental Mathematics, 31:2 (2022), 364-382

مصطلحات موضوعية: Mathematics - Algebraic Geometry, Computer Science - Logic in Computer Science, Mathematics - Logic, 14A15, 14-04, 03B16, 03B35, 68V20, G.m

URL الوصول: http://arxiv.org/abs/2104.09366

المؤلفون: Eberl, Manuel, Bordg, Anthony, Paulson, Lawrence C., Li, Wenda

المساهمون: Manuel Eberl and Anthony Bordg and Lawrence C. Paulson and Wenda Li

مصطلحات موضوعية: Isabelle/HOL, number theory, complex analysis, formalisation of mathematics

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.40

الاتاحة: https://doi.org/10.4230/LIPIcs.ITP.2024.40
https://nbn-resolving.org/urn:nbn:de:0030-drops-207686
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.40

المؤلفون: Bordg, Anthony, Lachnitt, Hanna, He, Yijun

مصطلحات موضوعية: Computer Science - Logic in Computer Science, Quantum Physics, 03B35, 03B15, 81P68, 68Q12

URL الوصول: http://arxiv.org/abs/2012.13925

المؤلفون: Bordg, Anthony, He, Yijun

مصطلحات موضوعية: Quantum Physics, Computer Science - Information Theory, 81P40 81P45 91A05 91A10 91B80

URL الوصول: http://arxiv.org/abs/1911.09354

المؤلفون: Bordg, Anthony

Thesis Advisors: Nice, Hirschowitz, André

مصطلحات موضوعية: Fondations univalentes, Théorie homotopique des types, Axiome d'univalence, Catégories de modèles, Théorie de l'homotopie, Théorie des catégories, Préfaisceaux, Groupoïdes, Univers, Univalent foundations, Homotopy type theory, Univalence axiom, Quillen model categories, Homotopy theory, Category theory, Presheaves, Groupoids, Universe

الاتاحة: http://www.theses.fr/2015NICE4083

المؤلفون: Bordg, Anthony

مصطلحات موضوعية: Mathematics - Category Theory, Mathematics - Algebraic Topology, Mathematics - Logic

URL الوصول: http://arxiv.org/abs/1712.03409

المؤلفون: Bordg, Anthony

مصطلحات موضوعية: Mathematics - Category Theory, Mathematics - Algebraic Topology, Mathematics - Logic, 55P

URL الوصول: http://arxiv.org/abs/1712.02652

المؤلفون: Bordg, Anthony

المصدر: In: Centrone S., Kant D., Sarikaya D. (eds) Reflections on the Foundations of Mathematics. Synthese Library, vol 407, 2019. Springer, Cham

مصطلحات موضوعية: Mathematics - Logic, Computer Science - Logic in Computer Science, 03B15 03B35

URL الوصول: http://arxiv.org/abs/1710.02723

المؤلفون: Bordg, Anthony

مصطلحات موضوعية: Mathematics - Category Theory, Mathematics - Logic

URL الوصول: http://arxiv.org/abs/1710.02028

المؤلفون: Bordg, Anthony

المصدر: Bordg, Anthony (2019) Univalent Foundations and the UniMath Library. The Architecture of Mathematics. in Reflections on the Foundations of Mathematics, Synthese Library, 407.

وصف الملف: text

Relation: https://philsci-archive.pitt.edu/16639/; https://www.springer.com/gp/book/9783030156541

المؤلفون: Bordg, Anthony

المصدر: Bordg, Anthony (2018) Univalent Foundations and the UniMath Library. The Architecture of Mathematics. [Preprint]

وصف الملف: text

Relation: https://philsci-archive.pitt.edu/15057/

المؤلفون: Bordg, Anthony

المصدر: Bordg, Anthony (2018) Univalent Foundations and the UniMath Library. [Preprint]

وصف الملف: text

Relation: https://philsci-archive.pitt.edu/15034/

المؤلفون: Bordg, Anthony

مصطلحات موضوعية: Mathematics - Category Theory, Mathematics - Algebraic Topology, Mathematics - Logic

URL الوصول: http://arxiv.org/abs/1512.04083

المؤلفون: Bordg, Anthony

المساهمون: European Research Council

المصدر: The Mathematical Intelligencer ; volume 43, issue 4, page 48-52 ; ISSN 0343-6993 1866-7414

الاتاحة: http://dx.doi.org/10.1007/s00283-020-10037-7
https://link.springer.com/content/pdf/10.1007/s00283-020-10037-7.pdf
https://link.springer.com/article/10.1007/s00283-020-10037-7/fulltext.html

المؤلفون: Manuel Eberl, Bordg, Anthony, Paulson, Lawrence C., Wenda Li

Relation: https://github.com/pruvisto/Number_Theory_ITP2024/tree/itp2024_camera_ready; https://doi.org/10.5281/zenodo.12586103; https://doi.org/10.5281/zenodo.12586104; oai:zenodo.org:12586104

الاتاحة: https://doi.org/10.5281/zenodo.12586104

المؤلفون: Bordg, Anthony, Doña Mateo, Adrián

المساهمون: ERC

المصدر: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

الاتاحة: http://dx.doi.org/10.1145/3573105.3575679
https://dl.acm.org/doi/pdf/10.1145/3573105.3575679

المؤلفون: Bordg, Anthony

المساهمون: Grantová Agentura České Republiky

المصدر: Applied Categorical Structures ; volume 27, issue 3, page 311-322 ; ISSN 0927-2852 1572-9095

الاتاحة: http://dx.doi.org/10.1007/s10485-019-09558-w
http://link.springer.com/article/10.1007/s10485-019-09558-w/fulltext.html
http://link.springer.com/content/pdf/10.1007/s10485-019-09558-w.pdf

المؤلفون: Aczel, Peter, Ahrens, Benedikt, Altenkirch, Thorsten, Awodey, Steve, Barras, Bruno, Bauer, Andrej, Bertot, Yves, Bezem, Marc, Coquand, Thierry, Finster, Eric, Grayson, Daniel, Herbelin, Hugo, Joyal, André, Licata, Dan, Lumsdaine, Peter, Mahboubi, Assia, Martin-Löf, Per, Melikhov, Sergey, Pelayo, Alvaro, Polonsky, Andrew, Shulman, Michael, Sozeau, Matthieu, Spitters, Bas, van den Berg, Benno, Voevodsky, Vladimir, Warren, Michael, Angiuli, Carlo, Bordg, Anthony, Brunerie, Guillaume, Kapulkin, Chris, Rijke, Egbert, Sojakova, Kristina, Avigad, Jeremy, Cohen, Cyril, Constable, Robert, Curien, Pierre-Louis, Dybjer, Peter, Escardó, Martín, Hou, Kuen-Bang, Gambino, Nicola, Garner, Richard, Gonthier, Georges, Hales, Thomas, Harper, Robert, Hofmann, Martin, Hofstra, Pieter, Koch, Joachim, Kraus, Nicolai, Li, Nuo, Luo, Zhaohui, Nahas, Michael, Palmgren, Erik, Riehl, Emily, Scott, Dana, Scott, Philip, Soloviev, Sergei

المساهمون: University of Manchester Manchester, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Functional Programming Laboratory, University of Nottingham, UK (UON), Carnegie Mellon University Pittsburgh (CMU), Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX), École polytechnique (X), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS), University of Ljubljana, Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Institute for Advanced Study Princeton (IAS), Department of Computer Science and Engineering Göteborg (CSE), Chalmers University of Technology Göteborg, National Science Foundation Arlington (NSF), Design, study and implementation of languages for proofs and programs (PI.R2), Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Paris Cité (UPCité)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Stockholm University, Symbolic Special Functions : Fast and Certified (SPECFUN), Inria Saclay - Ile de France, Institute for the History and Philosophy of Science and Technology (IHPST), University of Toronto, Russian Foundation for Basic Research (RFBR), Washington University in Saint Louis (WUSTL), San Diego State University (SDSU), Institute for Computing and Information Sciences Nijmegen (ICIS), Radboud University Nijmegen, Institute for Logic, Language and Computation (ILLC), Universiteit van Amsterdam (UvA), Univerzita Karlova Praha, Česká republika = Charles University Prague, Czech Republic (UK), Laboratoire Jean Alexandre Dieudonné (LJAD), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA), University of Western Ontario (UWO), Cornell University New York, University of Birmingham Birmingham, School of Mathematics Leeds, University of Leeds, Department of Pure Mathematics and Mathematical Statistics (DPMMS), Faculty of mathematics Centre for Mathematical Sciences Cambridge (CMS), University of Cambridge UK (CAM)-University of Cambridge UK (CAM), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation Redmond, Wash., Institut für Informatik München/Munich (LMU), Ludwig Maximilian University Munich = Ludwig Maximilians Universität München (LMU), Department of Mathematics and Statistics Ottawa, University of Ottawa Ottawa, Johannes Gutenberg - Universität Mainz = Johannes Gutenberg University (JGU), Baylor College of Medicine (BCM), Baylor University, Department of Computer Science (Royal Holloway University of London), Computer Learning Research Centre Royal Holloway, University of London, Royal Holloway University of London (RHUL)-Royal Holloway University of London (RHUL), Department of Mathematics Stockholm University, Swedish Academy, Princeton University

المصدر: https://inria.hal.science/hal-00935057 ; The Univalent Foundations Program Institute for Advanced Study, pp.1--587, 2013 ; https://hott.github.io/book/hott-ebook-7-g6913a1a.pdf.

مصطلحات موضوعية: ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT], [MATH.MATH-LO]Mathematics [math]/Logic [math.LO]

الاتاحة: https://inria.hal.science/hal-00935057

المؤلفون: Bordg, Anthony, Lachnitt, Hanna, He, Yijun

مصطلحات موضوعية: Article, Isabelle/HOL, Certification, Quantum computing, No-cloning, Quantum teleportation, Deutsch’s algorithm, Deutsch–Jozsa algorithm, Quantum prisoner’s dilemma, 03B35, 03B15, 81P68, 68Q12

وصف الملف: text/xml; application/pdf

Relation: https://www.repository.cam.ac.uk/handle/1810/323375

الاتاحة: https://www.repository.cam.ac.uk/handle/1810/323375
https://doi.org/10.17863/CAM.70833