Abstract
Locales provide a module system for the Isabelle proof assistant. Recently, locales have been ported to the new Isar format for structured proofs. At the same time, they have been extended by locale expressions, a language for composing locale specifications, and by structures, which provide syntax for algebraic structures. The present paper presents both and is suitable as a tutorial to locales in Isar, because it covers both basics and recent extensions, and contains many examples. © Springer-Verlag 2004.
Cite
CITATION STYLE
Ballarin, C. (2004). Locales and locale expressions in Isabelle/Isar. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3085, 34–50. https://doi.org/10.1007/978-3-540-24849-1_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
