Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477652zbMATHOpenAlexFDO

Authors

Publication date 6 July 2006

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

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

Mathematics Subject Classification ID

Recommendations

• Constructive Type Classes in Isabelle
• Formal verification of monad transformers
• HOLCF = HOL + LCF
• Free theorems involving type constructor classes, functional pearl
• scientific article; zbMATH DE number 2185697

Cited in

(8)

• Imperative Functional Programming with Isabelle/HOL
• Effect polymorphism in higher-order logic (proof pearl)
• Formal verification of monad transformers
• Constructive Type Classes in Isabelle
• Effect polymorphism in higher-order logic (proof pearl)
• First-Class Type Classes
• Secure Microkernels, State Monads and Scalable Refinement
• A Purely Definitional Universal Domain

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Theorem Proving in Higher Order Logics

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