The nomination singles out the following contributions by Huet.
Congratulations to Huet and to French TCS, which has given and still gives important contributions to our field.
- In the early 70's, Huet developed both resolution and unification for higher-order logic: these results have became the core of several modern systems that perform deduction in higher-order logic.
- Huet has done fundamental research in the areas of rewriting and Knuth-Bendix completion. His writings in this area are extensive and elegant. - Between 1982 and 1989, Huet directed and contributed to the design and implementation of the CAML functional programming language. That language and its descendants have given academics and industries an efficient and well structured programming language.
- In the 1990s, Huet and his students designed and built the first version of the Coq proof assistant. Today, Coq is one of the most used and trusted platforms for formalized mathematics and formal methods.
2 comments:
Hi Luca,
There's a follow-up post on this subject on the Computational Complexity blog; I have a comment there. Perhaps you would like to add something? (I found the post mildly disturbing, and I sense you have struggled similarly on this issue in the past :).)
Hi Avik,
Thanks a lot for the pointer and for writing a very well worded, may I say "mature", comment to the that post. I have just added my two-cent worth to the discussion.
And yes, I have struggled with similar issues in the past :-)
Post a Comment