Locales and Locale Expressions in Isabelle/Isar
Locales and Locale Expressions in Isabelle/Isar
复制标题
Isabelle/Isar 中的区域设置和区域设置表达式
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
C. Ballarin
中科院分区：
文献类型：
--
作者：
C. Ballarin
locale为Isabelle验证助手提供了一个模块系统。最近，区域设置已被移植到新的Isar格式，用于结构化证明。同时，语言环境表达式（一种用于组合语言环境规范的语言）和结构（为代数结构提供语法）对它们进行了扩展。本文介绍了这两种语言环境，并且适合作为Isar语言环境的教程，因为它涵盖了基础和最新的扩展，并包含许多示例。
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.