Now showing items 17-36 of 59

• #### A Conversation with Tim Teitelbaum ﻿

(Internet-First University Press, 2015-09-10)
A discussion of the teaching of large, introductory courses in programming in the early days-using the Terak and Macintosh computers and the development of integrated programming environments that implement language-aware ...
• #### Current Ideas on Programming Methodology ﻿

(Cornell University, 1976-07)
NO ABSTRACT SUPPLIED
• #### Describing an Algorithm by Hopcroft ﻿

(Cornell University, 1972-12)
We give an algorithm, its correctness proof, and its proof of execution time bound, for finding the sets of equivalent states in a deterministic finite state automaton. The time bound is $K\cdotm\cdot\n\cdot\\log n$ where ...
• #### Developing a Linear Algorithm for Cubing a Cyclic Permutation ﻿

(Cornell University, 1986-09)
A linear algorithm is developed for cubing a cyclic permutation stored as a function in an array. This continues work discussed in [0] and [1] on searching for disciplined methods for developing and describing algorithms ...
• #### Developing Two of Arsac's Funny Algorithms ﻿

(Cornell University, 1985-11)
In Some Funny Program (Ecole Normale Superieure, Paris, June 1985) J. Arsac discusses several algorithms, but not from the standpoint of their development. Here, we develop the algorithms given their specification using ...
• #### Educating the Programmer: Notation, Proofs, and the Development of Programs ﻿

(Cornell University, 1980-04)
The current state of affairs in programming is discussed. The opinion is expressed that effective programming requires more "mathematical maturity" than most programmers have. Further, education in formal logicc, which ...
• #### Engineering: Cornell Quarterly, Vol.20, No.2 (Autumn 1985): Twenty Years of Computer Science at Cornell ﻿

(Internet-First University Press, 1985)
IN THIS ISSUE: Twenty Years of Computer Science at Cornell /2 David Gries ... Immediate Computation or How to Keep a Personal Computer Busy /12 Tim Teitelbaum and Thomas Reps ... Reaching Agreement: A Fundamental Task Even ...
• #### Equational Propositional Logic ﻿

(Cornell University, 1994-09)
We formalize equational propositional logic, prove that it is sound and complete, and compare the equational-proof style with the more traditional Hilbert style.

(Cornell University, 1983-09)
A distributed program is presented that ensures delivery of a message to the functioning processors in a computer network, despite the fact that processors may fail at any time. All processor failures are assumedd to be ...
• #### Finding Repeated Elements ﻿

(Cornell University, 1982-07)
Two algorithms are presented for finding the values that occur more than $n \div k$ times in array b[O:n-1]. The second algorithm requires time $O(n \log(k))$ and extra space $O(k)$. We prove that $O(n \log(k))$ is a ...
• #### Formal Justification of Underspecification for S5 ﻿

(Cornell University, 1997-02)
We formalize the notion of underspecification as a means of avoiding problems with partial functions in modal logic S5 and some semantically related logics. For these logics, underspecification respects validity, so ...
• #### Formal versus semiformal proof in teaching predicate logic ﻿

(Cornell University, 1996-08)
This space is left deliberately non-blank
• #### Formalizations Of Substitution Of Equals For Equals ﻿

(Cornell University, 1998-05)
Inference rule "substitution of equals for equals" has been formalized in terms of simple substitution (which performs a replacement even though a free occurrence of a variable is captured), contextual substitution (which ...
• #### General Correctness: A Unification of Partial and Total Correctness ﻿

(Cornell University, 1984-10)
General correctness, which subsumes partial and total correctness, is defined for both weakest preconditions and strongest postconditions. Healthiness properties for general-correctness predicate transformers are more ...
• #### Generating a Random Cyclic Permutation ﻿

(Cornell University, 1986-09)
ABSTRACT NOT SUPPLIED
• #### The Hopcroft-Tarjan Planarity Algorithm, Presentation and Improvements ﻿

(Cornell University, 1988-04)
We give a rigorous, yet, we hope, readable, presentation of the Hopcroft-Tarjan linear algorithm for testing the planarity of a graph, using more modern principles and techniques for developing and presenting algorithms ...
• #### In-situ Inversion of a Cyclic Permutation ﻿

(Cornell University, 1985-09)
An algorithm is developed for the in-situ inversion of a cyclic permutation represented in an array. The emphasis is on the quo modo rather than the quod; we are interested in finding concepts and notations for dealing ...
• #### Inorder Traversal of a Binary Tree and its Inversion ﻿

(Cornell University, 1987-11)
ABSTRACT NOT AVAILABLE
• #### An Introduction to Proofs of Program Correctness for Teachers of College-Level Introductory Programming Courses ﻿

(Cornell University, 1990-03)
No abstract is available.
• #### Is Sometimes Ever Better Than Always? ﻿

(Cornell University, 1978-06)
The "intermittent assertion" method for proving programs correct is explained and compared to the conventional axiomatic method. Simple axiomatic proofs of iterative algorithms that compute recursively defined functions, ...