Local Theory Specifications in Isabelle/Isar

DOI10.1007/978-3-642-02444-3_10MaRDI QIDQ3638251zbMATH OpenOpenAlexFDO

Authors Florian Haftmann, Makarius Wenzel

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

Recommendations

• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Types for Proofs and Programs
• scientific article; zbMATH DE number 1614689
• Locales: a module system for mathematical theories
• Tutorial to locales and locale interpretation

Cites work

• A formulation of the simple theory of types
• A theory of type polymorphism in programming
• Building Formal Method Tools in the Isabelle/Isar Framework
• Constructive Type Classes in Isabelle
• Context Aware Calculation and Deduction
• scientific article; zbMATH DE number 1082080 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof-assistants using dependent type systems
• Structured formal development in Isabelle
• Theorem proving in higher order logics. 10th international conference, TPHOLs '97. Murray Hill, NJ, USA. August 19--22, 1997. Proceedings
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Types for Proofs and Programs

Cited in

(18)

• A modular first formalisation of combinatorial design theory
• Exploring the structure of an algebra text with locales
• From LCF to Isabelle/HOL
• Priority inheritance protocol proved correct
• Locales: a module system for mathematical theories
• scientific article; zbMATH DE number 1614689 (Why is no real title available?)
• Automated Reasoning in Higher-Order Regular Algebra
• Three chapters of measure theory in Isabelle/HOL
• Packaging Mathematical Structures
• The Isabelle Framework
• Constructive Type Classes in Isabelle
• Types for Proofs and Programs
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Reasoning about memory layouts
• A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
• Anselm's God in Isabelle/HOL
• Conditional Transfer Rule

Describes a project that uses

Uses Software

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

This page was built for publication: Local Theory Specifications in Isabelle/Isar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3638251)