School of Computing

Structure and properties of traces for functional programs

Olaf Chitil and Yong Luo

In Ian Mackie, editor, Proceedings of the 3rd International Workshop on Term Graph Rewriting, Termgraph 2006, ENTCS, pages 182-196. Elsevier, April 2007.

Abstract

The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace can then be viewed in various ways to support program comprehension and debugging. The trace was named the augmented redex trail. Its structure was inspired by standard graph rewriting implementations of functional languages. Here we describe a model of the trace that captures its essential properties and allows formal reasoning. The trace is a graph constructed by graph rewriting but goes beyond simple term graphs. Although the trace is a graph whose structure is independent of any rewriting strategy, we define the trace inductively, thus giving us a powerful method for proving its properties.

Download publication 262 kbytes (PDF)

Bibtex Record

@inproceedings{2509,
author = {Olaf Chitil and Yong Luo},
title = {Structure and Properties of Traces for Functional Programs},
month = {April},
year = {2007},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2007/2509},
    publication_type = {inproceedings},
    submission_id = {21416_1176294325},
    booktitle = {Proceedings of the 3rd International Workshop on Term Graph Rewriting, Termgraph 2006},
    editor = {Ian Mackie},
    series = {ENTCS},
    publisher = {Elsevier},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014