Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
From MaRDI portal
Publication:5200125
DOI10.1007/978-3-642-22673-1_20zbMath1335.68223MaRDI QIDQ5200125
Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Silvio Valentini, Giovanni Sambin
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
Uses Software
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