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;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.
Lecture Notes in Computer Science
278
280
Asperti, Andrea; Maietti, M. E.; SACERDOTI COEN, Claudio; Sambin, G.; Valentini, S.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/105074
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact