Sciweavers

TPHOL
2002
IEEE
13 years 11 months ago
Weakest Precondition for General Recursive Programs Formalized in Coq
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 ...
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu
TPHOL
2002
IEEE
13 years 11 months ago
Quotient Types: A Modular Approach
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...
Aleksey Nogin
TPHOL
2002
IEEE
13 years 11 months ago
Type-Theoretic Functional Semantics
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...
Yves Bertot, Venanzio Capretta, Kuntal Das Barman
TPHOL
2002
IEEE
13 years 11 months ago
The 5 Colour Theorem in Isabelle/Isar
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...
Gertrud Bauer, Tobias Nipkow
TPHOL
2002
IEEE
13 years 11 months ago
A Proposal for a Formal OCL Semantics in Isabelle/HOL
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...
Achim D. Brucker, Burkhart Wolff
TPHOL
2002
IEEE
13 years 11 months ago
Free-Style Theorem Proving
g Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 ...
David Delahaye