PRL Seminars 1998-99

Listening to Theorem Provers who Talk to Each Other about Computer Systems


Robert Constable





October 20, 1998




Abstract

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.