Towards a topos theoretic foundation for the Irish School of Constructive Mathematics (Mc

Abstract

The Irish School of Constructive Mathematics (Mc ), which extends the VDM, exploits an algebraic notation based upon monoids and their morphisms for the purposes of abstract modelling. Its method depends upon an operator calculus. The School hereto eschewed every form of formal language and formal logic, relying solely upon constructive mathematics. In 1995 the School committed itself to the development of the modelling of (computing) systems in full generality. This was achieved by embracing Category Theory and by exploring a geometry of formal methods using techniques of fiber bundles. From fiber bundles to sheaves was a natural step. Concurrently, the School moved from the algebra of monoids to categories, and from categories to topoi. Finally, the constructive nature of the School is now coming to terms with formalism and logic through the (natural) intuitionistic logic inherently manifest through topoi. In this paper we exhibit an accessible bridge from classical formal methods to topos theoretic formal methods in seeking a unifying theory. © Springer-Verlag Berlin Heidelberg 2001.