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
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...
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...
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...
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...