HOL-Omega
From MaRDI portal
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
- Equational Reasoning with Applicative Functors
- On definitions of constants and types in HOL
- HOL Zero
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Verified characteristic formulae for CakeML
- Comprehending Isabelle/HOL’s Consistency
- Transfer
- Lifting
- HOL2P
- HALO
- HOLCF
- Tycon
- Stern-Brocot Tree
- Monomorphic Monad
- Applicative Lifting
- Meta Model Isabelle
- Perron Frobenius
- Effect polymorphism in higher-order logic (proof pearl)
This page was built for software: HOL-Omega
