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
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
Related Items
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