Now showing items 1-20 of 49

• #### A Causal Logic of Events in Formalized Computational Type Theory ﻿

(Cornell University, 2005-12-13)
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 correct-by-construction programming ...
• #### Computability on Continuous Higher Types and its Role in the Semantics of Programming Languages ﻿

(Cornell University, 1974-07)
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 ﻿

(Cornell University, 1988-03)
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 ﻿

(2008-10-15)
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 ﻿

(Cornell University, 1970-11)
One point made here is that formal constructive mathematics can be interpreted as a "high-level" 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 ﻿

(Cornell University, 1983-05)
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 ﻿

(Cornell University, 1973-10)
NO ABSTRACT SUPPLIED
• #### A Conversation with Claire Cardie ﻿

(Internet-First University Press, 2015-09-09)
Claire Cardie discusses the role of Gerard Salton, natural language processing and the creation of the Information Science Department.
• #### A Conversation with David Gries ﻿

(Internet-First University Press, 2015-07-21)
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 ﻿

(Internet-First University Press, 2015-09-09)
Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc.
• #### A Conversation with Robert L. Constable ﻿

(Internet-First University Press, 2015-07-21)
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 ﻿

(Cornell University, 1982-10)
NO ABSTRACT SUPPLIED
• #### Effectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLP ﻿

(2008-10-15)
The Fischer-Lynch-Paterson 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 ﻿

(Cornell University, 1976-03)
The PL/CS language is an instructional variant of PL/C designed to provide a simple, easy-to-understand 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 ﻿

(Cornell University, 2006-01-27)
Mathematical and program-code 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 ﻿

(Cornell University, 1986-03)
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 ﻿

(Cornell University, 1980-06)
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 ﻿

(Cornell University, 1989-04)
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 ﻿

(Cornell University, 1986-03)
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 Martin-Lof's Intuitionistic Type Theory. We show how one can express the intuition that ...
• #### Investigations of Type Theory in Programming Logics and Intelligent Systems ﻿

(Cornell University, 1985-09)
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 ...