Projects per year
To investigate the use of VTLoE as a basis for formal derivation of functional programs with effects. As a part of the process, a number of issues central to effective formal programming are considered. In particular it is considered how to develop a proof system suitable for pratical reasoning, how to implement this system in the generic proof assistant Isabelle and finally how to apply the logic and the implementation to programming.
|Place of Publication||Kgs. Lyngby, Denmark|
|Publisher||Technical University of Denmark|
|Number of pages||170|
|Publication status||Published - Aug 1996|