Research Output 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.
|Effective start/end date||01/08/1991 → 01/07/1996|