Formalising Overlap Algebras in Matita

DOI10.1017/S0960129511000107zbMath1223.68102OpenAlexW2102919742MaRDI QIDQ3094175

Claudio Sacerdoti Coen, Enrico Tassi

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000107

zbMATH Keywords

Matitaalgebraic presentationformalisation of formal topologyoverlap algebras

Mathematics Subject Classification ID

Related Items (2)

Dynamics in Foundations: What Does It Mean in the Practice of Mathematics? ⋮ Towards ``mouldable code via nested code graph transformation

Uses Software

• Matita

Cites Work

• Spurious disambiguation errors and how to get rid of them
• The overlap algebra of regular opens
• A compact kernel for the calculus of inductive constructions
• The calculus of constructions
• Inductively generated formal topologies.
• The problem of the formalization of constructive topology
• User interaction with the Matita proof assistant
• Hints in Unification
• First-Class Type Classes
• Smart Matching
• The point of pointless topology
• Normalization and the Yoneda embedding
• Unnamed Item

This page was built for publication: Formalising Overlap Algebras in Matita