HCAR + Normalisation + Rewriting
Friday, April 28th, 2006 by James Chapman- Firstly here is the HCAR plan:

- Andreas Abel talked about writing a functional normalizer for
that is structurally recursive (on types) and is therefore terminating. He has submitted a paper on this topic to MSFP 2006 - Christoph Luth is visiting Neil this week. Neil talked about a very general principle about rewriting they are working on. See this for their most recent published paper on their approach to rewriting.