Skip to main content

4 Result(s)

within Rob Arthan Remove this filter Software Engineering 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 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)

  4. No Access

    Chapter

    HOL

    Statement

    John Harrison, Konrad Slind, Rob Arthan in The Seventeen Provers of the World (2006)