TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
Terminator is a static analysis tool developed by Microsoft Research for proving termination of Windows device drivers written in C. This proof pearl describes a formalization in h...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
Techniques based on sums of squares appear promising as a general approach to the universal theory of reals with addition and multiplication, i.e. verifying Boolean combinations of...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
Abstract. We present a formal treatment of normalization by evaluation in type theory. The involved semantics of simply-typed λ-calculus is exactly the simply typed fragment of th...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
We propose a method to extract purely functional contents from logical inductive types in the context of the Calculus of Inductive Constructions. This method is based on a mode con...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
Abstract. We use the theorem prover Isabelle to formalise and machinecheck results of the theory of generalised substitutions given by Dunne and used in the B method. We describe t...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method tur...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
We formalise the data race free (DRF) guarantee provided by Java, as captured by the semi-formal Java Memory Model (JMM) [1] and published in the Java Language Specification [2]. ...
TPHOL
2007
IEEE
13 years 10 months ago
2007
IEEE
Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor...