School of Computing

Proving the correctness of algorithmic debugging for functional programs

Yong Luo and Olaf Chitil

In Trends in Functional Programming, volume 7, pages 182-196. Intellect Books, January 2007.

Abstract

This paper presents a formal 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 sufficiently general induction hypothesis.

Download publication 94 kbytes (PDF)

Bibtex Record

@inproceedings{2863,
author = {Yong Luo and Olaf Chitil},
title = {Proving the Correctness of Algorithmic Debugging for Functional Programs},
month = {January},
year = {2007},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2007/2863},
    publication_type = {inproceedings},
    submission_id = {5607_1231251555},
    booktitle = {Trends in Functional Programming},
    volume = {7},
    publisher = {Intellect Books},
}

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

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

Last Updated: 21/03/2014