{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T21:27:30Z","timestamp":1770413250501,"version":"3.49.0"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2011,8]]},"abstract":"<jats:p>We describe some formal topological results, formalised in Matita 1\/2, presented in predicative intuitionistic logic and in terms of Overlap Algebras.<\/jats:p><jats:p>Overlap Algebras are new algebraic structures designed to ease reasoning about subsets in an algebraic way within intuitionistic logic. We find that they also ease the formalisation of formal topological results in an interactive theorem prover.<\/jats:p><jats:p>Our main result is the existence of a functor between two categories of \u2018generalised topological spaces\u2019, one with points (Basic Pairs) and the other point-free (Basic Topologies). This formalisation is part of a wider scientific collaboration with the inventor of the theory, Giovanni Sambin. His goal is to verify in what sense his theory is \u2018implementable\u2019, and to discover what problems may arise in the process. We check that all intermediate constructions respect the stringent size requirements imposed by predicative logic. The formalisation is quite unusual, since it has to make explicit size information that is often hidden.<\/jats:p><jats:p>We found that the version of Matita used for the formalisation was largely inappropriate. The formalisation drove several major improvements of Matita that will be integrated in the next major release (Matita 1.0). We show some motivating examples, taken directly from the formalisation, for these improvements. We also describe a possibly sub-optimal solution in Matita 1\/2, which is exploitable in other similar systems. We briefly discuss a better solution available in Matita 1.0.<\/jats:p>","DOI":"10.1017\/s0960129511000107","type":"journal-article","created":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T14:53:35Z","timestamp":1309532015000},"page":"763-793","source":"Crossref","is-referenced-by-count":4,"title":["Formalising Overlap Algebras in Matita"],"prefix":"10.1017","volume":"21","author":[{"given":"CLAUDIO","family":"SACERDOTI COEN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ENRICO","family":"TASSI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2011,7,1]]},"reference":[{"key":"S0960129511000107_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2010.02.002"},{"key":"S0960129511000107_ref13","first-page":"386","volume-title":"Proceedings of LICS1989","author":"Luo","year":"1989"},{"key":"S0960129511000107_ref18","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.53.2"},{"key":"S0960129511000107_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002508"},{"key":"S0960129511000107_ref10","first-page":"88","volume-title":"Proceedings of MKM2004","author":"Cruz-Filipe","year":"2004"},{"key":"S0960129511000107_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-008-0058-2"},{"key":"S0960129511000107_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0003-3"},{"key":"S0960129511000107_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14128-7_23"},{"key":"S0960129511000107_ref12","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-1983-15080-2"},{"key":"S0960129511000107_ref19","first-page":"51","article-title":"A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita.","volume":"1","author":"Sacerdoti Coen","year":"2008","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129511000107_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9070-5"},{"key":"S0960129511000107_ref25","first-page":"530","volume-title":"Proceedings of TACS97","author":"Werner","year":"1997"},{"key":"S0960129511000107_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129511000107_ref22","first-page":"41","article-title":"A new look at generalized rewriting in type theory.","volume":"2","author":"Sozeau","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129511000107_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0960129511000107_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0960129511000107_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_16"},{"key":"S0960129511000107_ref1","first-page":"1","article-title":"A page in number theory.","volume":"1","author":"Asperti","year":"2008","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129511000107_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-004-0243-1"},{"key":"S0960129511000107_ref21","volume-title":"The Basic Picture: a structural basis for constructive topology","author":"Sambin","year":"2011"},{"key":"S0960129511000107_ref14","volume-title":"From sets and types to topology and analysis, toward a minimalist foundation for constructive mathematics","author":"Maietti","year":"2005"},{"key":"S0960129511000107_ref16","volume-title":"D\u00e9finitions inductives en th\u00e9orie des types d'ordre sup\u0155ieur","author":"Paulin-Mohring","year":"1996"},{"key":"S0960129511000107_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_7"},{"key":"S0960129511000107_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"S0960129511000107_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_9"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T07:26:57Z","timestamp":1556350017000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000107\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,1]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["S0960129511000107"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000107","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,1]]}}}