HOL-Omega
The HOL-Omega logic A new logic is posited for the widely used HOL theorem prover, as an extension of the existing higher order logic of the HOL4 system. The logic is extended to three levels, adding kinds to the existing levels of types and terms. New types include type operator variables and universal types as in System $F$. Impredicativity is avoided through the stratification of types by ranks according to the depth of universal types. The new system, called HOL-Omega or $mathrm{HOL} _{omega }$, is a merging of HOL4, HOL2P, and major aspects of System $F _{omega }$ from Chapter 30 of [{it B. C. Pierce}, Types and programming languages. Cambridge: MIT Press (2002)]. This document presents the abstract syntax and semantics for the kinds, types, and terms of the logic, as well as the new fundamental axioms and rules of inference. As the new logic is constructed according to the design principles of the LCF approach, the soundness of the entire system depends critically and solely on the soundness of this core.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
Sorted by year (- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Lochbihler, Andreas: Effect polymorphism in higher-order logic (proof pearl) (2019)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
- Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
- Arthan, Rob: On definitions of constants and types in HOL (2016)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
- Lochbihler, Andreas; Schneider, Joshua: Equational reasoning with applicative functors (2016)
- Homeier, Peter V.: The HOL-Omega logic (2009)