Sciweavers

BIRTHDAY
2004
Springer

Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework

13 years 9 months ago
Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
Abstract. The logical and operational aspects of rewriting logic as a logical framework are tested and illustrated in detail by representing pure type systems as object logics. More precisely, we apply membership equational logic, the equational sublogic of rewriting logic, to specify pure type systems as they can be found in the literature and also a new variant of pure type systems with explicit names that solves the problems with closure under α-conversion in a very satisfactory way. Furthermore, we use rewriting logic itself to give a formal operational description of type checking, that directly serves as an efficient type checking algorithm. The work reported here is part of a more ambitious project concerned with the development of the open calculus of constructions, an equational extension of the calculus of constructions that incorporates rewriting logic as a computational sublanguage. This paper is a detailed study on the ease and naturalness with which a family of higher-or...
Mark-Oliver Stehr, José Meseguer
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where BIRTHDAY
Authors Mark-Oliver Stehr, José Meseguer
Comments (0)