Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita

DOI10.1007/978-3-642-22673-1_20zbMath1335.68223OpenAlexW17079225MaRDI QIDQ5200125

Giovanni Sambin, Andrea Asperti, Claudio Sacerdoti Coen, Maria Emilia Maietti, Silvio Valentini

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_20

Mathematics Subject Classification ID

Related Items (1)

Dynamics in Foundations: What Does It Mean in the Practice of Mathematics?

Uses Software

• Matita

Cites Work

• The overlap algebra of regular opens
• A minimalist two-level foundation for constructive mathematics
• Cantor theorem and friends, in logical form
• User interaction with the Matita proof assistant
• Non-uniform (hyper/multi)coherence spaces
• Zen and the art of formalisation
• Constructive version of Boolean algebra

This page was built for publication: Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita