Preprints & Publications
The classification below is somewhat arbitrary, since some of these papers could possibly fit more than one topic.
Mathematics:
Algebraic structures:
The Interpretation Lifting Theorem for C-systems, Theory and Applications of Categories, Vol. 38, 2022, No. 7, article.
Homotopical structures:
On a Model Invariance Problem in Homotopy Type Theory, Applied Categorical Structures, 2019, article.
On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom, 23 pages. arXiv:1712.0265
Books:
Homotopy Type Theory : Univalent Foundations of mathematics, as part of The Univalent Foundations Program, Institute for Advanced Study, Princeton, 2013. book freely available online
Expository writing:
What is a Scheme in Algebraic Geometry? A Problem-Oriented Approach, draft
Computer science:
Journal articles:
with Lawrence Paulson and Wenda Li, Simple Type Theory is not too Simple: Grothendieck's schemes without dependent types, Experimental Mathematics, 2022, article
with Hanna Lachnitt and Yijun He, Certified Quantum Computation in Isabelle/HOL, Journal of Automated Reasoning, 65(5), 691-709, 2020 (arXiv version)
with Yijun He, Comment on "Quantum Games and Quantum Strategies", 2019, arXiv:1911.09354
Workshop and conference refereed articles:
with Manuel Eberl, Lawrence Paulson and Wenda Li, Formalising Half of a Graduate Textbook in Number Theory, to appear in ITP 2024.
with Adrian Dona Mateo, Encoding Dependently-Typed Constructions into Simple Type Theory, CPP 2023, article.
with Yiannos Stathopoulos and Lawrence Paulson, A Parallel Corpus for Natural Language Machine Translation to Isabelle, CICM 2022, article available in the following proceedings.
with Nicolo Cavalleri, Elements of Differential Geometry in Lean, CEUR Workshop Proceedings of FMM 2021, the Fifth Workshop on Formal Mathematics for Mathematicians (part of CICM 2021), article.
Refereed book chapters:
Univalent Foundations and the UniMath Library : The Architecture of Mathematics, in Reflections on the Foundations of Mathematics, Synthese Library, 407, 2019, Springer. arXiv:1710.02723
Refereed extended abstracts:
with Yiannos Stathopoulos and Lawrence Paulson, A Parallel Corpus of Natural Language and Isabelle Artefacts, AITP 2022, abstract
Computer code:
Strict Omega Categories , Archive of Formal Proofs, 2023.
Grothendieck's Schemes in Algebraic Geometry , Archive of Formal Proofs, 2021.
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information, Archive of Formal Proofs, 2020.
The Localization of a Commutative Ring, Archive of Formal Proofs, 2018.
Projective Geometry, Archive of Formal Proofs, 2018.
Things with ideas:
A Tale of Duality, Letter to the Editor, Notices of the American Mathematical Society, 69(1), January 2022, pdf
Hypercriticality, Hypocriticality and Hyperempathy, Letter to the Editor, Communications of the ACM, 64(12), December 2021, online version
A Replication Crisis in Mathematics? The Mathematical Intelligencer (2021)
Some Slides:
A Parallel Corpus for Autoformalisation, IRIF, November 21th 2022, slides
Machine Learning and Autoformalisation, LMF, November 16th 2022, slides
How to Do Maths without Dependent Types, IHES, June 15th 2022, slides
Textbooks:
with Alice Erlinger and Vincent Nolot, L'épreuve de mathématiques à Sciences Po, Ellipses, 2016, 304 pages (math textbook in French).
Translations:
with Julien Cantegreil et al, L'Ecole de New Haven de droit international, Editions A.Pedone, 2010. (International Law)