7 Result(s)
-
Article
Open AccessSelf-Formalisation of Higher-Order Logic
We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem...
-
Article
Open AccessOn Definitions of Constants and Types in HOL
This paper reports on a simpler and more powerful replacement for the principles for defining new constants that were previously provided in the various HOL implementations. We discuss the problems that the ne...
-
Chapter and Conference Paper
HOL Constant Definition Done Right
This note gives a proposal for a simpler and more powerful replacement for the mechanisms currently provided in the various HOL implementations for defining new constants.
-
Chapter and Conference Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation
We present a mechanised semantics and soundness proof for the HOL Light kernel including its definitional principles, extending Harrison’s verification of the kernel without definitions. Soundness of the logic...
-
Chapter
(Dual) Hoops Have Unique Halving
Continuous logic extends the multi-valued Łukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The sema...
-
Chapter and Conference Paper
The 1st Verified Software Competition: Experience Report
We, the organizers and participants, report our experiences from the 1st Verified Software Competition, held in August 2010 in Edinburgh at the VSTTE 2010 conference.
-
Chapter
HOL
Statement
