University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > Extending deforestation

Extending deforestation

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

We present a technique to perform fully automated functional program simplifications beyond what is possible through ordinary deforestation. Our implementation can so far do simplifications such as “length (insert_sort xs) => length xs” and “reverse (reverse xs) => xs”. As our last property shows, these simplifications are for eagerly evaluated functional programs.

We will also show a correspondence between our extended deforestation, and automated proof in dependent type theory. In effect one can use the same algorithm to both find a simplification, and prove that the simplification is sound.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity