Local Theory Specifications in Isabelle/Isar

DOI10.1007/978-3-642-02444-3_10zbMath1246.68197OpenAlexW1561420154MaRDI QIDQ3638251

Makarius Wenzel, Florian Haftmann

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02444-3_10

Mathematics Subject Classification ID

Related Items

A modular first formalisation of combinatorial design theory ⋮ Packaging Mathematical Structures ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ Reasoning about memory layouts ⋮ Exploring the structure of an algebra text with locales ⋮ Unnamed Item ⋮ The Isabelle Framework ⋮ From LCF to Isabelle/HOL ⋮ Priority inheritance protocol proved correct ⋮ Three Chapters of Measure Theory in Isabelle/HOL ⋮ Locales: a module system for mathematical theories

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Isabelle/Isar
• Isar
• HOL
• Locales

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of type polymorphism in programming
• Theorem proving in higher order logics. 10th international conference, TPHOLs '97. Murray Hill, NJ, USA. August 19--22, 1997. Proceedings
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Building Formal Method Tools in the Isabelle/Isar Framework
• Constructive Type Classes in Isabelle
• Context Aware Calculation and Deduction
• Types for Proofs and Programs
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• A formulation of the simple theory of types