Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch
English
 

Publications Search - Details

 
Publication type: Article
Author: Maksym Bortin, Einar Broch Johnsen, Christoph Lüth
Title: Structured Formal Development in Isabelle
Volume: 12
Page(s): 1 – 20
Journal: Nordic Journal of Computing
Year published: 2006
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.
PDF Version: http://www.informatik.uni-bremen.de/~cxl/papers/njc06.pdf
PostScript Version: http://www.informatik.uni-bremen.de/~cxl/papers/njc06.ps.gz
Status: Reviewed
Last updated: 27. 04. 2007

 Back to result list
 
   
Author: Automatically generated page
 
  Group BKB 
Last updated: May 9, 2023   impressum