Email Gateway (Aug 22 2022 at 21:08): Email Gateway (Aug 22 2022 at 21:08):From: Clemens Ballarin <ballarin@in.tum.de>
I am pleased to announce another report on locales:
Clemens Ballarin. Exploring the Structure of an Algebra Text with
Locales. Journal of Automated Reasoning, 2019,
http://dx.doi.org/10.1007/s10817-019-09537-9
At the core of the paper is a case study, which has led to a number of
improvements to locales. A discussion of approaches to algebra in
Isabelle and HOL provers follows. The paper provides guidance on using
locales and identifies patterns of use. It complements my earlier
report, which was focussed on how locales work:
Clemens Ballarin. Locales: a module system for mathematical theories.
Journal of Automated Reasoning, 52(2):123–153, 2014,
http://dx.doi.org/10.1007/s10817-013-9284-7
The case study itself is in the AFP. Author's versions of the papers
can be downloaded from my TUM web page.
Clemens
Last updated: Apr 24 2024 at 01:07 UTC