Structured Formal Development in Isabelle

Abstract. General purpose theorem provers provide advanced facilities for proving properties about specifications, and may therefore be a valuable tool in formal program development. However, these provers generally lack many of the useful structuring mechanisms found in functional programming or specification languages. This paper presents a constructive approach to adding theory morphisms and parametrisation to theorem provers, while preserving the proof support and consistency of the prover. The approach is implemented in Isabelle and illustrated by examples of an algorithm design rule and of the modular development of computational effects for imperative language features based on monads. ACM CCS Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic; I.2.2 [Artificial Intelligence]: Automatic Programming. Key words: Program development, t...

• Type: Journal
• Year: 2006
• Where: NJC
• Authors: Maksym Bortin, Einar Broch Johnsen, Christoph Lüth
• Keywords: General Purpose Theorem, NJC 2006, Program Development, Provers