© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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}, }