The HOL-Omega Logic

DOI10.1007/978-3-642-03359-9_18zbMath1252.68257OpenAlexW1493683612MaRDI QIDQ3183533

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

Related Items

On definitions of constants and types in HOL ⋮ From types to sets by local type definition in higher-order logic ⋮ Friends with Benefits ⋮ Verified Characteristic Formulae for CakeML ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ HOL-Omega ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Equational Reasoning with Applicative Functors

Uses Software

• HOL
• HOL2P

Cites Work

• The \(HOL\) logic extended with quantification over type variables
• The formal theory of monads. II
• HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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