This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
The IA-64 architecture defers floating point and integer division to software. To ensure correctness and maximum efficiency, Intel provides a number of recommended algorithms which...
This paper outlines a formal model of the Intel IA-64 architecture, and explains how this model can be used to verify the correctness of assembly-level code optimizations. The form...
We modify the reflection method to enable it to deal with partial functions like division. The idea behind reflection is to program a tactic for a theorem prover not in the impleme...
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasonin...
We verify within the Coq proof assistant that ML typing is sound with respect to the dynamic semantics. We prove this property in the framework of a big step semantics and also in ...
We provide a proof using HOL and SPIN of convergence for the Routing Information Protocol (RIP), an internet protocol based on distance vector routing. We also calculate a sharp re...
Karthikeyan Bhargavan, Carl A. Gunter, Davor Obrad...
Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and re...