Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68521OpenAlexW2484880499MaRDI QIDQ5477652FDOQ5477652

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

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

Mathematics Subject Classification ID

Cited In (8)

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

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)