TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is RN with the...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
The Verisoft project aims at the pervasive formal verification of entire computer systems. In particular, the seamless verification of the academic system is attempted. This syst...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
We have definitionally extended Isabelle/HOLCF to support axiomatic Haskell-style constructor classes. We have subsequently defined the functor and monad classes, together with t...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
Abstract. We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
Abstract. How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? We propose an initial set of b...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
We show that delaying fully-expansive proof reconstruction for non-interactive decision procedures can result in a more efficient workflow. In contrast with earlier work, our appr...