ITP
2010
13 years 8 months ago
2010
Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)ind...
ITP
2010
13 years 8 months ago
2010
Abstract. We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functi...
ITP
2010
13 years 8 months ago
2010
Abstract. In order to make existing formalizations available for settheoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This c...
ITP
2010
13 years 8 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
13 years 8 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
13 years 8 months ago
2010
ITP
2010
13 years 8 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
13 years 8 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
13 years 8 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
13 years 8 months ago
2010