KnowledgeBase » 
SEMINAR
» ID = 288
Listening to Theorem Provers who Talk to Each Other about Computer Systems
by Robert L. Constable
1998-1999
I would like to try out the talk I plan to give this week at CMU.
The talk tries to illustrate applications of semantic theory to systems. It is mainly an excuse for talking about Jason's very dependent type and the coding of dependent records and Howe's work on relating HOL and Nuprl --- including some observations that Evan and I have made about relating PVS and Nuprl.
I also try to mention the work of Amanda and Regina on natural language translations.
None of the results is new to the seminar, but my spin on them is.