ITP
2010
14 years 4 months ago
2010
We present a formalisation of separation logic which, by avoiding the use of existential quantifiers, allows proofs that only use standard equational rewriting methods as found in...
ITP
2010
14 years 4 months ago
2010
Abstract. Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive...
ITP
2010
14 years 4 months ago
2010
ITP
2010
14 years 4 months ago
2010
Abstract. This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. This is a modern RISC architecture with many advanced features. The f...
ITP
2010
14 years 4 months ago
2010
Abstract. We present a new scheme to translate mathematical developments from HOL Light to Coq, where they can be re-used and rechecked. By relying on a carefully chosen embedding ...
ITP
2010
14 years 4 months ago
2010
In this paper, we develop a general theory of fixed point combinators, in higher-order logic equipped with Hilbert’s epsilon operator. This combinator allows for a direct and e...
ITP
2010
14 years 4 months ago
2010
ITP
2010
14 years 4 months ago
2010
Abstract. The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of these proofs in the theorem provers...
ITP
2010
14 years 4 months ago
2010
ITP
2010
14 years 4 months ago
2010
CertiCrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the code-based paradigm, in which the statement ...