HOL-Omega

swMATH6581MaRDI QIDQ18673FDOQ18673

Author name not available (Why is that?)

Described by source

• The HOL-Omega Logic

Cited In (8)

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

This page was built for software: HOL-Omega