Email Gateway (Aug 19 2022 at 10:51): Email Gateway (Aug 19 2022 at 10:51):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Users of Isabelle,
I'm pleased to announce a new paper on locales:
Locales: a Module System for Mathematical Theories
Journal of Automated Reasoning, Springer
http://dx.doi.org/10.1007/s10817-013-9284-7
I would like to use this occasion to summarize the other literature
most relevant to locale users:
The Tutorial (see http://isabelle.in.tum.de/documentation.html)
This is the obvious starting point.
The Isabelle/Isar Reference Manual
(also see http://isabelle.in.tum.de/documentation.html)
This is the complete reference to syntax and technical details of
the implementation (including its limitations).
The new paper complements the two by presenting a concise view of how
locales work. For the abstract, please see below.
Clemens
Locales are a module system for managing theory hierarchies in
a theorem prover through theory interpretation. They are available
for the theorem prover Isabelle. In this paper, their semantics is
defined in terms of local theories and morphisms.
Locales aim at providing flexible means of extension and reuse.
Theory modules (which are called locales) may be extended by
definitions and theorems. Interpretation to Isabelle's global
theories and proof contexts is possible via morphisms. Even the
locale hierarchy may be changed if declared relations between locales
do not adequately reflect logical relations, which are implied by the
locales' specifications.
By discussing their design and relating it to more commonly known
structuring mechanisms of programming languages and provers, locales
are made accessible to a wider audience beyond the users of Isabelle.
The discussed mechanisms include ML-style functors, type classes and
mixins (the latter are found in modern object-oriented languages).
Last updated: Apr 26 2024 at 08:19 UTC