© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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, pages 182-196. 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 = {182-196}, keywords = {determinacy analysis, Craig interpolants}, 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}, }