School of Computing

Proving the correctness of algorithmic debugging for functional programs

Olaf Chitil and Yong Luo

In Pre-Proceedings of the Seventh Symposium on Trends in Functional Programming, TFP 2006. University of Nottingham, April 2006.

Abstract

This paper formally presents a model of tracing for functional programs based on a small-step operational semantics. The model records the computation of a functional program in a graph which can be utilised for various purposes such as algorithmic debugging. The main contribution of this paper is to prove the correctness of algorithmic debugging for functional programs based on the model. Although algorithmic debugging for functional programs is implemented in several tracers such as Hat, the correctness has not been formally proved before. The difficulty of the proof is to find a suitable induction principle and a more general induction hypothesis.

Download publication 78 kbytes (PDF)

Bibtex Record

@inproceedings{2473,
author = {Olaf Chitil and Yong Luo},
title = {Proving the Correctness of Algorithmic Debugging for Functional Programs},
month = {April},
year = {2006},
pages = {},
keywords = {augmented redex trail},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2006/2473},
    publication_type = {inproceedings},
    submission_id = {8215_1170269204},
    organization = {University of Nottingham},
    booktitle = {Pre-Proceedings of the Seventh Symposium on Trends in Functional Programming, TFP 2006},
}

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

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

Last Updated: 23/06/2011 17:22