This is a collection of technical reports from the Cornell's Computer Science (CS) Department from the time period of 1968-2002. These reports are part of the NCSTRL collection of Computer Science Technical Reports.

For reports from 2003-present, see the Computing and Information Science Technical Reports Collection.

Recent Submissions

  • Type-Theoretic Methodology for Practical Programming Languages 

    Crary, Karl (Cornell University, 1998-08)
    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 "Correct-by-Construction" DecisionProcedures from Constructive Proofs 

    Caldwell, James (Cornell University, 1998-12)
    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, 1975-07)
    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, 1983-10)
    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, 1972-08)
    In Chapter I of this paper we show that the usual, textbook pairing functions have decidable first-order 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, 1995-09)
    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, 1992-09)
    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, 1989-12)
    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, 1976-09)
    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, 1980-02)
    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 ...

View more


RSS Feeds