arXiv Open Access 2021

Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types

Anthony Bordg Lawrence Paulson Wenda Li

Lihat Sumber

Abstrak

Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the simple type theory of the proof assistant Isabelle/HOL, and we discuss the design choices which make this work possible. We show in the particular case of schemes how the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales.

Topik & Kata Kunci

math.AG cs.LO math.LO

Penulis (3)

Anthony Bordg

Lawrence Paulson

Wenda Li

Format Sitasi

APA MLA BibTeX

Bordg, A., Paulson, L., Li, W. (2021). Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types. https://arxiv.org/abs/2104.09366

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2021
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓