PRL Seminars

Mark-Oliver Stehr presented two brief and related talks.

Abstract

Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics

We present the essence of the HOL-Nuprl connection using terminology from general logics (Meseguer 87). We consider the HOL-Nuprl connection as composed of two parts, an automatic translation between axiomatic HOL and Nuprl theories and an interactive part interpreting an axiomatic Nuprl theory in classical Nuprl. The justification is done on the level of entailment systems which gives a very strong semantic independent correctness result.

Abstract

Type Theory in a Membership Equational Logic Framework

We propose the use of Membership Equational Logic (Bouhoula, Jouannaud, Meseguer 97) as a framework for higher-order type theories. We present a development of the Calulus of Constructions with some extensions as a running example using the Maude rewriting engine.