Modular reasoning in Isabelle

DOI10.1007/10721959_7MaRDI QIDQ2723411zbMATH OpenFDO

Authors Florian Kammüller

Publication date 5 July 2001

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

Full work available at URL https://doi.org/10.1007/10721959_7

Mathematics Subject Classification ID

Recommendations

• Modular structures as dependent types in Isabelle
• Types for Proofs and Programs
• Tutorial to locales and locale interpretation
• Local Theory Specifications in Isabelle/Isar
• Exploring the structure of an algebra text with locales

Cited in

(13)

• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• Exploring the structure of an algebra text with locales
• Locales: a module system for mathematical theories
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Tutorial to locales and locale interpretation
• The Isabelle Framework
• Local Theory Specifications in Isabelle/Isar
• Modular structures as dependent types in Isabelle
• Fixed points theorems for non-transitive relations
• Logic-Free Reasoning in Isabelle/Isar
• Types for Proofs and Programs
• scientific article; zbMATH DE number 7649979 (Why is no real title available?)
• Complete Non-Orders and Fixed Points

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Modular reasoning in Isabelle

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