DagRep.8.8.130.pdf
- Filesize: 11.17 MB
- 16 pages
Document
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)
Authors and all authors of the abstracts in this report
-
Part of:
Issue:
Dagstuhl Reports, Volume 8, Issue 8
Volume: Dagstuhl Reports, Volume 8
Journal: Dagstuhl Reports (DagRep) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-02-22
Cite AsGet BibTex
Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). In Dagstuhl Reports, Volume 8, Issue 8, pp. 130-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/DagRep.8.8.130
https://doi.org/10.4230/DagRep.8.8.130
Abstract
Formalized mathematics is mathematical knowledge (definitions, theorems, and proofs) represented in digital form suitable for computer processing. The central goal of this seminar was to identify the theoretical advances and practical improvements needed in the area of formalized mathematics, in order to make it a mature technology, truly useful to a larger community of students and researchers in mathematics. During the seminar, various software systems for formalization were compared, and potential improvements to existing systems were investigated. There have also been discussions on the representation of algebraic structures in formalization systems.
Keywords
- formal methods
- formalized mathematics
- proof assistant
- type theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads