Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

CONSTRUCTIVE MATHEMATICS AS A PROGRAMING LOGIC 1: SOME PRINCIPLES OF THEORY

IP.com Disclosure Number: IPCOM000127980D
Original Publication Date: 1983-Dec-31
Included in the Prior Art Database: 2005-Sep-14
Document File: 13 page(s) / 42K

Publishing Venue

Software Patent Institute

Related People

Robert L. Constable: AUTHOR [+3]

Abstract

The design of a programming system is guided by certain beliefs, princi-ples and practical constraints. These considerations are not always manifest from the rules defining the system.' In this paper the author discusses some of t he principles which have guided 'the design of the programing.logics built at Cornell' in the last decade. Most of the necessarily brief, discussion con-cerns type theory with stress on the concepts of function space and quotient types.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 10% of the total text.

Page 1 of 13

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

CONSTRUCTIVE MATHEMATICS AS A PROGRAMING LOGIC 1: SOME PRINCIPLES OF THEORY

Robert L. Constable

TR 83-554 May 1983

Department of Computer Science Cornell University Ithaca, New York This work was supported in part by NSF grants MCS-80-03349 and MCS-81-04018.

Abstract

The design of a programming system is guided by certain beliefs, princi-ples and practical constraints. These considerations are not always manifest from the rules defining the system.' In this paper the author discusses some of t he principles which have guided 'the design of the programing.logics built at Cornell' in the last decade. Most of the necessarily brief, discussion con-cerns type theory with stress on the concepts of function space and quotient types.

Key Words and Phrases:

automated logic* combinators, Edinburgh LCF. partial recursive func-tions. programing languages and logics, PL/CV, PRL, propositions-as-types, quotient types. strong intensionality. type theory.

I. Introduction

How do we choose the languages in which to express exact reasoning. mathematics and programing? In the case of logic and mathema. tics. language has evolved. over a period of perhaps 2,000 years. We know enough to say that such language is not the "God-given expression of Truth". Indeed human genius, especially that of Frege, has played a major role. , In the case of progrmming languages the period of evolution is shorter. It might appear dramatically shorter, but if we consider the building of relatively rigorous and symbolic languages then perhaps only the last 100 years are relevant even

This work was supported in part by NSF grants MCS-80-03349 and MCS-81-04018. for mathematics and logic. Although we can learn a great deal from this period, not many formal languages from it were meant to be used; fewer still were in fact used. By contrast in the past 40 years hundreds of progranming languages have been created, each vying for prominence. Among these a few dozen are serious contenders with distinct characteristics, e.g. FORTRAN. ALGOL (60, W, 68), LISP, PL/I. ADA. etc. How then are these languages chosen? What are the principles of design that make them attractive, usable and endur-ing?

Cornell University Page 1 Dec 31, 1983

Page 2 of 13

CONSTRUCTIVE MATHEMATICS AS A PROGRAMING LOGIC 1: SOME PRINCIPLES OF THEORY

There have been studies which atteupt to sort out the principles behind such languages [321. But not many deep principles have emerged. We can clas-sify languages based on their control structures and make illuminating com-parisons [9,281. We can discuss procedure calling mechanisms and other features of implementation. With more modern languages we can comp*are type structures and mechanisms for achieving modularity and protection.

While these differences among progrmming languages are fascinating and while their study may contribute to better designs and implementations, such differences do not reveal d...