TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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 ...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...
TPHOL
2000
IEEE
14 years 4 months ago
2000
IEEE
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...