Archive for April, 2006

HCAR + Normalisation + Rewriting

Friday, April 28th, 2006 by James Chapman
  • Firstly here is the HCAR plan:
    hcar
  • Andreas Abel talked about writing a functional normalizer for \lambda^\rightarrow 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.