What's new?

• Alan has submitted his thesis (September 2010)
• Amy and Brigitte's benchmarks for HOAS [Coq scripts].
  
• Journal paper finally accepted (May 2010).
• Hybrid (in Coq) proves properties of open terms, viz type uniqueness for PCF, 2009.
• Isabelle/HOL 2008 porting of Hybrid (by  Alan Martin). September 08.