KnowledgeBase » 
SEMINAR
» ID = 492
Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics and Type Theory in a Membership Equational Logic Framework
by Mark-Oliver Stehr
1998-1999
Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics
and
Type Theory in a Membership Equational Logic Framework
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.