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