Sciweavers

Share
TPHOL
2008
IEEE
8 years 9 months ago
Certifying a Termination Criterion Based on Graphs, without Graphs
Although graphs are very common in computer science, they are still very difficult to handle for proof assistants as proving properties of graphs may require heavy computations. T...
Pierre Courtieu, Julien Forest, Xavier Urbain
TPHOL
2008
IEEE
8 years 9 months ago
Canonical Big Operators
In this paper, we present an approach to describe uniformly iterated “big” operations, like Pn i=0 f(i) or maxi∈I f(i) and to provide lemmas that encapsulate all the commonly...
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioa...
TPHOL
2008
IEEE
8 years 9 months ago
Nominal Inversion Principles
When reasoning about inductively defined predicates, such as typing judgements or reduction relations, proofs are often done by inversion, that is by a case analysis on the last r...
Stefan Berghofer, Christian Urban
TPHOL
2008
IEEE
8 years 9 months ago
Formal Reasoning About Causality Analysis
Systems that can immediately react to their inputs may suffer from cyclic dependencies between their actions and the corresponding trigger conditions. For this reason, causality an...
Jens Brandt, Klaus Schneider
TPHOL
2008
IEEE
8 years 9 months ago
A Type of Partial Recursive Functions
We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises...
Ana Bove, Venanzio Capretta
TPHOL
2008
IEEE
8 years 9 months ago
A Brief Overview of HOL4
The HOL4 proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an o...
Konrad Slind, Michael Norrish
TPHOL
2008
IEEE
8 years 9 months ago
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correc...
Daniel Wasserrab, Andreas Lochbihler
TPHOL
2008
IEEE
8 years 9 months ago
An ACL2 Tutorial
We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to...
Matt Kaufmann, J. Strother Moore
TPHOL
2008
IEEE
8 years 9 months ago
First-Class Type Classes
Abstract. Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specith abstract structures by quantification o...
Matthieu Sozeau, Nicolas Oury
books