Recommendations
Cites work
- scientific article; zbMATH DE number 42431 (Why is no real title available?)
- scientific article; zbMATH DE number 88983 (Why is no real title available?)
- A Brief Overview of HOL4
- Axiom of Choice and Complementation
- Completeness in the theory of types
- HOL Constant Definition Done Right
- HOL Light: An Overview
- HOL with definitions: semantics, soundness, and a verified implementation
- Interactive theorem proving from the perspective of Isabelle/Isar
- Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
- Structured theory development for a mechanized logic
- The HOL-Omega Logic
- Towards Self-verification of HOL Light
- Z
Cited in
(9)- Comprehending Isabelle/HOL’s Consistency
- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- Model-theoretic conservative extension for definitional theories
- On the two definitions of Ho(pro C)
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
- Stateless HOL
- From LCF to Isabelle/HOL
- A consistent foundation for Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: On definitions of constants and types in HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287358)
