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

DOI10.1080/10586458.2022.2062073zbMath1498.14001arXiv2104.09366OpenAlexW3156224329MaRDI QIDQ5094472

Wenda Li, Anthony Bordg, Lawrence Charles Paulson

Publication date: 3 August 2022

Published in: Experimental Mathematics (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2104.09366

zbMATH Keywords

sheavestype theoryschemeshigher order logiclogic and verification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to algebraic geometry (14-04) Schemes and morphisms (14A15) Formalization of mathematics in connection with theorem provers (68V20) Research data for problems pertaining to algebraic geometry (14-11)

Related Items (2)

Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL

Uses Software

• Coq
• Isabelle/HOL
• Coquelicot
• Locales
• Lean

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• From types to sets by local type definition in higher-order logic
• Coquelicot: a user-friendly library of real analysis for Coq
• Exploring the structure of an algebra text with locales
• Locales: a module system for mathematical theories
• The Lean Theorem Prover (System Description)
• Algebraically Closed Fields in Isabelle/HOL
• Schemes in Lean
• A Machine-Checked Proof of the Odd Order Theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• A formulation of the simple theory of types

This page was built for publication: Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types