Skip to main content

4 Result(s)

within Rob Arthan Remove this filter Logics and Meanings of Programs Remove this filter

and

  1. No Access

    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.

    Rob Arthan in Interactive Theorem Proving (2014)

  2. No Access

    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...

    Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens in Interactive Theorem Proving (2014)

  3. No Access

    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...

    Rob Arthan, Paulo Oliva in Automated Reasoning and Mathematics (2013)

  4. No Access

    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.

    Vladimir Klebanov, Peter Müller, Natarajan Shankar… in FM 2011: Formal Methods (2011)