TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
Abstract. This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is ...
TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a speci...
TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given b...
TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
Based on an inductive definition of triangulations, a theory of undirected planar graphs is developed in Isabelle/HOL. The proof of the 5 colour theorem is discussed in some detai...
TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
Abstract We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardizatio...
TPHOL
2002
IEEE
14 years 4 months ago
2002
IEEE
g Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 ...