The HOL-Omega Logic

DOI10.1007/978-3-642-03359-9_18MaRDI QIDQ3183533zbMATH OpenOpenAlexFDO

Authors Peter V. Homeier

Publication date 20 October 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-03359-9_18

Mathematics Subject Classification ID

Recommendations

• The \(HOL\) logic extended with quantification over type variables
• The higher-order-logic Formath
• scientific article; zbMATH DE number 2185697
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• scientific article; zbMATH DE number 1424012

Cites work

• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• scientific article; zbMATH DE number 733401 (Why is no real title available?)
• scientific article; zbMATH DE number 977284 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3318613 (Why is no real title available?)
• The \(HOL\) logic extended with quantification over type variables
• The formal theory of monads. II
• Types and programing languages

Cited in

(17)

• From types to sets by local type definition in higher-order logic
• HOL-Omega
• From types to sets by local type definitions in higher-order logic
• Equational Reasoning with Applicative Functors
• On definitions of constants and types in HOL
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Verified characteristic formulae for CakeML
• Comprehending Isabelle/HOL’s Consistency
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• Edmonds-Karp
• Flow Networks
• Gabow SCC
• Stateless higher-order logic with quantified types
• Prpu_Maxflow
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)
• The higher-order-logic Formath

Describes a project that uses

Uses Software

• HOL
• HOL2P

This page was built for publication: The HOL-Omega Logic

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