|
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/6394
| Title: | Constructive Mathematics as a Programming Logic I: Some Principles of Theory |
| Authors: | Constable, Robert L. |
| Keywords: | computer science
technical report |
| Issue Date: | May-1983 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR83-554 |
| Abstract: | The design of a programming system is guided by certain beliefs, principles, and practical constraints. These considerations are not always manifest from the rules defining the system. In this paper, the author discusses some of the principles which have guided the design of the programming logics built at Cornell in the last decade. Most of the necessarily brief discussion concerns type theory with stress on the concepts of function space and quotient types. Key Words and Phrases: automated logic, combinators, Edinburgh LCF, partial recursive functions, programming languages and logics, PL/CV, PRL, propositions-as-types, quotient types, strong intensionality, type theory. |
| URI: | http://hdl.handle.net/1813/6394 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
