College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||Nuprl as a General Logic|
|Authors: ||Constable, Robert L.|
Howe, Douglas J.
|Keywords: ||computer science|
|Issue Date: ||Jun-1989|
|Publisher: ||Cornell University|
|Abstract: ||Study of the architecture and design of proof development systems has become important lately as their use has spread and become closely tied to programming environments. One of the central issues is how to provide a general framework for defining and using a variety of logics in such systems; in particular, whether it is better to staart with a simple core system, such as the typed lambda-calculus with dependent function types, or start with a very rich theory providing a formalized metatheory. The first approach is exemplified by the Edinburgh LF. Here we illustrated the second approach by showing how to use Nuprl as a framework for defining logics in the style of the LF. Central to the viability of the second apprroach is a method of showing that the encoding of user defined logics in Nuprl is faithful. This paper presents a new semantic method to solve the problem. The method is applicable to the LF as well, and seems simpler than the syntactic methods that previously were used and which seem to hinder the use of rich thoeries as logical frameworks.|
|Appears in Collections:||Computer Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.