Got cut elimination working in the HLF implementation for additive conjunction, and multiplicative unit! That makes six "connectives" that work, now, 1, top, bottom, ampersand, trivial, and atoms. I am super stoked. I am slightly cheating, since I am making use of monotonicity without checking it, but it's a very heartening proof-of-concept. Also, I finally got around to checking it in as a real branch rather than in my own subversion repository. It is at https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-hlf/
My INBOX contains two items, both pertinent to the immediate future. Doin' that inbox zero thing. We'll see if it Changes My Life.