TPHOL
2002
IEEE
14 years 11 days 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 11 days 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 11 days 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 11 days 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 11 days 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 11 days ago
2002
IEEE
g Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 ...