License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.8.8.130
URN: urn:nbn:de:0030-drops-102370
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10237/
Go back to Dagstuhl Reports

Bauer, Andrej ; Escardó, Martín ; Lumsdaine, Peter L. ; Mahboubi, Assia
Weitere Beteiligte (Hrsg. etc.): Andrej Bauer and Martín H. Escardó and Peter L. Lumsdaine and Assia Mahboubi

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)

pdf-format:
dagrep_v008_i008_p130_18341.pdf (11 MB)

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.

BibTeX - Entry

@Article{bauer_et_al:DR:2019:10237,
  author =	{Andrej Bauer and Mart{\'i}n Escard{\'o} and Peter L. Lumsdaine and Assia Mahboubi},
  title =	{{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}},
  pages =	{130--155},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{8},
  number =	{8},
  editor =	{Andrej Bauer and Mart{\'i}n H. Escard{\'o} and Peter L. Lumsdaine and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10237},
  URN =		{urn:nbn:de:0030-drops-102370},
  doi =		{10.4230/DagRep.8.8.130},
  annote =	{Keywords: formal methods, formalized mathematics, proof assistant, type theory}
}

Keywords: formal methods, formalized mathematics, proof assistant, type theory
Collection: Dagstuhl Reports, Volume 8, Issue 8
Issue Date: 2019
Date of publication: 22.02.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI