Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types

References

• Ballarin, C. (2006). Interpretation of locales in isabelle: Theories and proof contexts. In: Borwein, J. M., Farmer, W. M., eds. International Conference on Mathematical Knowledge Management. Berlin: Springer, pp. 31–43.
   Google Scholar
• Ballarin, C. (2014). Locales: A module system for mathematical theories. J. Autom. Reason. 52(2): 123–153.
   Web of Science ®Google Scholar
• Ballarin, C. (2020). Exploring the structure of an algebra text with locales. J. Autom. Reason. 64(6): 1093–1121.
   Web of Science ®Google Scholar
• Boldo, S., Lelay, C., Melquiond, G. (2015). Coquelicot: A user-friendly library of real analysis for coq. Math. Comput. Sci. 9(1): 41–62.
   Google Scholar
• Bordg, A., Paulson, L., Li, W. (2021). Grothendieck’s schemes in algebraic geometry. Archive of Formal Proofs, March 2021. Available at https://isa-afp.org/entries/Grothendieck_Schemes.html, Formal proof development.
   Google Scholar
• Buzzard, K., Hughes, C., Lau, K., Livingston, A., Mir, R. F., Morrison, S. (2021). Schemes in Lean. Available at https://arxiv.org/abs/2101.02602. doi:https://doi.org/10.1080/10586458.2021.1983489
   Google Scholar
• Chicli, L. I. (2003). Sur la Formalisation des Mathématiques dans le Calcul des Constructions inductives. PhD thesis. Université Côte d’Azur. 2003NICE4088.
   Google Scholar
• Church, A. (1940). A formulation of the simple theory of types. J. Symb. Logic 5: 56–68. doi:https://doi.org/10.2307/2266170
   Google Scholar
• The Coq Development Team. The Coq Proof Assistant Reference Manual. Available at http://coq.inria.fr.
   Google Scholar
• Coquand, T., Huet, G. (1986). The calculus of constructions. PhD thesis. INRIA.
   Google Scholar
• Coquand, T., Paulin, C. (1988). Inductively defined types. In: Martin-Löf, P., Mints, G., eds. International Conference on Computer Logic. Berlin: Springer, pp. 50–66.
   Google Scholar
• de Moura, L., Kong, S., Avigad, J., Van Doorn, F., von Raumer, J. (2015). The lean theorem prover (system description). In: International Conference on Automated Deduction. Springer, pp. 378–388.
   Google Scholar
• de Vilhena, P. E., Paulson, L. C. (2020). Algebraically closed fields in Isabelle/HOL. In: International Joint Conference on Automated Reasoning. Springer pp. 204–220.
   Google Scholar
• Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Biha, S. O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L. (2013). A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., and Pichardie, D., eds, Interactive Theorem Proving. Berlin: Springer, pp. 163–179.
   Google Scholar
• Grothendieck, A. (1960). Éléments de géométrie algébrique: I. le langage des schémas. Publications Mathématiques de l’IHÉS, 4: 5–228.
   Google Scholar
• Hartshorne, R. (1977). Algebraic Geometry. Graduate Texts in Mathematics. New York: Springer.
   Google Scholar
• Hölzl, J., Immler, F., and Huffman, B. (2013). Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D., eds. ITP, LNCS 7998. Springer, pp. 279–294.
   Google Scholar
• Kobayashi, H., Chen, L., Murao, H. (2004). Groups, rings and modules. Archive of Formal Proofs, May 2004. Available at https://isa-afp.org/entries/Group-Ring-Module.html, Formal proof development.
   Google Scholar
• Kunčar, O., Popescu, A. (2019). From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2): 237–260.
   Web of Science ®Google Scholar
• Lang, S. (2002). Algebra. Graduate Texts in Mathematics. New York: Springer.
   Google Scholar
• Lee, H. (2014). Vector spaces. Archive of Formal Proofs. Available at https://isa-afp.org/entries/VectorSpace.html, Formal proof development.
   Google Scholar
• Nipkow, T., Paulson, L. C., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Berlin: Springer. Available at http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf.
   Google Scholar
• The Stacks Project Authors. (2018). Stacks Project. Available at https://stacks.math.columbia.edu.
   Google Scholar
• Wenzel, M. (1997). Type classes and overloading in higher-order logic. In Gunter, E. L., and Felty, A., eds. Theorem Proving in Higher Order Logics: TPHOLs ’97, LNCS 1275. Berlin: Springer, pp. 307–322.
   Google Scholar