HOL-Omega
From MaRDI portal
Software:18673
swMATH6581MaRDI QIDQ18673FDOQ18673
Author name not available (Why is that?)
Cited In (8)
- 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
- 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
