Extending deforestation

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

• William Sonnex (University of Cambridge)
• Tuesday 06 March 2012, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.