The project entitled “Formalization of Formal Topology by means of the interactive theorem prover Matita” is an official bilateral project between the Universities of Padova and Bologna, funded by the former, active from March 2008 until August 2010. The project aimed to bring together and exploit the synergic collaboration of two communities of researchers, both centered around constructive type theory: on one side the Logic Group at the University of Padova, focused on developing formal, pointfree topology within a constructive and predicative framework; on the other side, the Helm group at the University of Bologna, developing the Matita Interactive Theorem Prover, a young proof assistant based on the Calculus of Inductive Constructions as its logical foundation.
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita / Asperti, Andrea; Maietti, M. E.; SACERDOTI COEN, Claudio; Sambin, G.; Valentini, S.. - STAMPA. - 6824:(2011), pp. 278-280. (Intervento presentato al convegno Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011. tenutosi a Bertinoro, Italy, nel 18-23 Luglio 2011) [10.1007/978-3-642-22673-1_20].
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.
ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO;
2011
Abstract
The project entitled “Formalization of Formal Topology by means of the interactive theorem prover Matita” is an official bilateral project between the Universities of Padova and Bologna, funded by the former, active from March 2008 until August 2010. The project aimed to bring together and exploit the synergic collaboration of two communities of researchers, both centered around constructive type theory: on one side the Logic Group at the University of Padova, focused on developing formal, pointfree topology within a constructive and predicative framework; on the other side, the Helm group at the University of Bologna, developing the Matita Interactive Theorem Prover, a young proof assistant based on the Calculus of Inductive Constructions as its logical foundation.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
