TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
Abstract. Denotational semantics for a substantial fragment of Java is formalized by deep embedding in PVS, making extensive use of dependent types. A static analyzer for secure in...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem provin...
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
TPHOL
2005
IEEE
14 years 5 months ago
2005
IEEE
The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, whe...
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...