HOL-Omega

swMATH6581MaRDI QIDQ18673FDOQ18673

Author name not available (Why is that?)

Official website: http://trustworthytools.com/id17.html

Described by source

• The HOL-Omega Logic

Cited In (20)

• From types to sets by local type definition in higher-order logic
• From types to sets by local type definitions in higher-order logic
• Verified characteristic formulae for CakeML
• On definitions of constants and types in HOL
• HOL Zero
• HALO
• Lifting
• HOL2P
• Transfer
• HOLCF
• Tycon
• Applicative Lifting
• Meta Model Isabelle
• Monomorphic Monad
• Perron Frobenius
• Stern-Brocot Tree
• Equational Reasoning with Applicative Functors
• Effect polymorphism in higher-order logic (proof pearl)
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Comprehending Isabelle/HOL’s Consistency

This page was built for software: HOL-Omega