JavaScript is disabled for your browser. Some features of this site may not work without it.
Computer Science Technical Reports
Browse by
This is a collection of technical reports from the Cornell's Computer Science (CS) Department from the time period of 19682002. These reports are part of the NCSTRL collection of Computer Science Technical Reports.
For reports from 2003present, see the Computing and Information Science Technical Reports Collection.
Recent Submissions

TypeTheoretic Methodology for Practical Programming Languages
Crary, Karl (Cornell University, 199808)The significance of type theory to the theory of programming languages has long been recognized. Advances in programming languages have often derived from understanding that stems from type theory. However, these ... 
Decidability Extracted: Synthesizing "CorrectbyConstruction" DecisionProcedures from Constructive Proofs
Caldwell, James (Cornell University, 199812)The topic of this thesis is the extraction of efficient and readable programs from formal constructive proofs of decidability. The proof methods employed to generate the efficient code are new and result in clean and ... 
Axiomatic Proof Techniques for Parallel Programs
Owicki, Susan S. (Cornell University, 197507)This thesis presents an axiomatic method for proving certain correctness properties of parallel programs. Axioms and inference rules for partial correctness are given for two parallel programming languages: The General ... 
The Ultimate Planar Convex Hull Algorithm ?
Kirkpatrick, David G.; Seidel, Raimund (Cornell University, 198310)We present a new planar convex hull algorithm with worst case time complexity $O(n \log H)$ where $n$ is the size of the input set and $H$ is the size of the output set, i.e. the number of vertices found to be on the ... 
Decidable Pairing Functions
Tenney, Richard Lee (Cornell University, 197208)In Chapter I of this paper we show that the usual, textbook pairing functions have decidable firstorder theories. This will be done by exhibiting an infinite axiomatization of certain pairing functions which we characterize ... 
Implementation Issues in an Open Architectural Framework for Digital ObjectServices
Lagoze, Carl; Ely, David (Cornell University, 199509)We provide high level designs for implementing some key aspects of the Kahn/Wilensky Framework for Distributed Digital Object Services. We focus on five aspects of the architecture: 1) Negotiation on terms and conditions ... 
A Generalization of Brooks' Theorem
Srinivasan, Aravind (Cornell University, 199209)Given a connected graph $G = (V, E)$ with $n$ vertices and maximum degree $\Delta$ such that $\Delta \geq$ 3 and $G$ is not a complete graph, Brooks' theorem shows that $G$ is $\Delta$colorable. We prove a generalization ... 
Can LCF Be Topped? Flat Lattice Models of Typed $\lambda$Calculus
Bloom, Bard (Cornell University, 198912)Plotkin, [Plo77], examines the denotational semantics of PCF (essentially typed $\lambda$calculus with arithmetic and looping). The standard Scott semantics $\bigvee$ is computationally adequate but not fully abstract; ... 
Language Features for Process Interaction
Andrews, Gregory R.; McGraw, James R. (Cornell University, 197609)Language for parallel programming should meet four goals: expressiveness, reliability, security, and verifiability. This paper presents a set of language features for describing processes and process interaction, gives ... 
An Analysis of the Total Least Squares Problem
Golub, Gene H.; Van Loan, Charles (Cornell University, 198002)Totla least squares (TLS) is a method of fitting that is appropriate when there are errors in both the observation vector $b (mxl)$ and in the data matrix $A (mxn)$. The technique has been discussed by several authors ...