Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6821
Title: Nuprl as a General Logic
Authors: Constable, Robert L.
Howe, Douglas J.
Keywords: computer science
technical report
Issue Date: Jun-1989
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1021
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.
URI: http://hdl.handle.net/1813/6821
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
89-1021.pdf671.7 kBAdobe PDFView/Open
89-1021.ps185.71 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us