School of Computing

Lecture notes on formal program development

Stefan Kahrs

LFCS Report ECS-LFCS-97-372, University of Edinburgh, November 1997.


This document was originally produced as lecture notes for the MSc and PG course ``Formal Program Development'' early in 1997. After some initial general considerations on this subject the paper focusses on the way one can use Extended ML (EML) for formal program development, which features EML contains and why, and which pitfalls one has to avoid when formally developing ML programs. Usage, features, and pitfalls are all presented through examples.

Download publication 115 kbytes

Bibtex Record

author = {Stefan Kahrs},
title = {Lecture Notes on Formal Program Development},
month = {November},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    institution = {University of Edinburgh},
    number = {ECS-LFCS-97-372},
    type = {LFCS Report},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014