JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Constable, Robert L."
Now showing items 120 of 49

A Causal Logic of Events in Formalized Computational Type Theory
Bickford, Mark; Constable, Robert L. (Cornell University, 20051213)We provide a logic for distributed computing that has the explanatory and technical power of constructive logics of computation. Inparticular, we establish a proof technology that supports correctbyconstruction programming ... 
Computability on Continuous Higher Types and its Role in the Semantics of Programming Languages
Constable, Robert L.; Egli, Herbert (Cornell University, 197407)This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. In the process if constructing computable Scott models of the lambda calculus we examine the ... 
Computational Foundations of Basic Recursive Function Theory
Constable, Robert L.; Smith, Scott Fraser (Cornell University, 198803)The theory of computability, or basic recursive function theory as it is often called, is usually motivated and developed using Church's Thesis. Here we show that there is an alternative computability theory in which some ... 
Computational Type Theory
Constable, Robert L. (20081015)Computational type theory provides answers to questions such as: What is a type? What is a natural number? How do we compute with types? How are types related to sets? Can types be elements of types? How are data types ... 
Constructive Mathematics and Automatic Program Writers
Constable, Robert L. (Cornell University, 197011)One point made here is that formal constructive mathematics can be interpreted as a "highlevel" programming language; another point is that there are good reasons for doing so. Among them is the fact that a theoretical ... 
Constructive Mathematics as a Programming Logic I: Some Principles of Theory
Constable, Robert L. (Cornell University, 198305)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 ... 
A Constructive Theory of Recursive Functions
Constable, Robert L. (Cornell University, 197310)NO ABSTRACT SUPPLIED 
A Conversation with Claire Cardie
Cardie, Claire; Constable, Robert L. (InternetFirst University Press, 20150909)Claire Cardie discusses the role of Gerard Salton, natural language processing and the creation of the Information Science Department. 
A Conversation with David Gries
Gries, David; Constable, Robert L. (InternetFirst University Press, 20150721)David Gries joined Cornell in 1969. He was chair of CS in the 1980s and associate dean of engineering for 8 years in the 2000s. His research was on compiler writing and areas related to formal programming methodology. ... 
A Conversation with Dexter Kozen
Kozen, Dexter; Constable, Robert L. (InternetFirst University Press, 20150909)Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc. 
A Conversation with Robert L. Constable
Constable, Robert L.; Gries, David (InternetFirst University Press, 20150721)Over 40 years ago, Bob Constable and his students started designing a logical language for specifying programming tasks and mathematical problems. The system, called Nuprl, is known since 1984 for being able to synthesize ... 
The Definition of $\mu$PRL
Bates, Joseph L.; Constable, Robert L. (Cornell University, 198210)NO ABSTRACT SUPPLIED 
Effectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLP
Constable, Robert L. (20081015)The FischerLynchPaterson theorem (FLP) says that it is impossible for processes in an asynchronous distributed system to achieve consensus on a binary value when a single process can fail. It is a widely cited theoretical ... 
An Elementary Formal Semantics for the Programming Language PL/CS
Constable, Robert L.; Donahue, James E. (Cornell University, 197603)The PL/CS language is an instructional variant of PL/C designed to provide a simple, easytounderstand tool to teach a disciplined style of programming (see [Conway 1976]). This report gives a complete formal semantic ... 
Enabling Large Scale Coherency Among Mathematical Texts
Allen, Stuart F.; Constable, Robert L. (Cornell University, 20060127)Mathematical and programcode text is unique because significant portions of it can be anchored to counterparts in formal logical theories that are implemented by computer systems. These systems check formal proofs for ... 
Formalized Metareasoning in Type Theory
Knoblock, Todd B.; Constable, Robert L. (Cornell University, 198603)In this paper we present two practical methods of formalizing the metatheory of constructive type theory and demonstrate how they would be used to improve the reasoning capabilities of formal problem solving systems such ... 
The Fundamental Theorem of Arithmetic in PL/CV2
Constable, Robert L. (Cornell University, 198006)This document is a section of formal elementary number theory leading up to a complete proof of the fundamental theorem of arithmetic. On the way to this result a large number of simple facts about integer division, prime ... 
Implementing Metamathematics as an Approach to Automatic Theorem Proving
Constable, Robert L.; Howe, Douglas J. (Cornell University, 198904)A simple but important algorithm used to support automated reasoning is called matching: given two terms it produces a substitution, if one exists, that maps the first term to the second. In this paper the matching ... 
Infinite Objects in Type Theory
Mendler, N. P.; Panangaden, Prakash; Constable, Robert L. (Cornell University, 198603)In this paper we show how infinite objects can be defined in a constructive type theory. The type theory that we use is a variant of MartinLof's Intuitionistic Type Theory. We show how one can express the intuition that ... 
Investigations of Type Theory in Programming Logics and Intelligent Systems
Constable, Robert L. (Cornell University, 198509)Type theory has become central to computer science because it deals with fundamental issues in programming languages, in programming methodology and specification languages, in automatic theorem proving and programming ...