Now showing items 1-20 of 59

    • The 711 Problem 

      Gries, David (Cornell University, 1982-05)
    • Adding the Everywhere Operator to Propositional Logic 

      Gries, David; Schneider, Fred B. (Cornell University, 1996-05)
      Sound and complete modal propositional logic C is presented, in which "P" has the interpretation "P is true in all states". The interpretation is already known as the Carnapian extension of S5. A new axiomatization for ...
    • An Algorithm for Processing Program Transformations 

      Efremidis, Sofoklis G.; Gries, David (Cornell University, 1993-10)
      An algorithm for processing program transformations as described by the transform construct is presented. The algorithm constructs a coordinate transformation of an abstract program based on a set of transforms and ...
    • Assignment to Subscripted Variables 

      Gries, David (Cornell University, 1977-03)
      The assignment b(r):=e is investigated using two axiomatic definitions in order to gain an understanding of the problems involved with using arrays. It is seen that assignment to array elements leads to many of the ...
    • Avoiding the Undefined by Underspecification 

      Gries, David; Schneider, Fred B. (Cornell University, 1995-05)
      We use the appeal of simplicity and an aversion to complexity in selecting a method for handling partial functions in logic. We conclude that avoiding the undefined by using underspecifi- cation is the preferred choice.
    • A calculational proof of Andrews's challenge 

      Gries, David (Cornell University, 1996-08)
      This space is left deliberately non-blank
    • Cand and Cor Before and Then or Else in Ada 

      Gries, David (Cornell University, 1979-11)
    • Complete, Trace-based, Network Proof Systems: An Advisor's Perspective 

      Gries, David (Cornell University, 1987-08)
    • Completeness and Incompleteness of Trace-Based Network Proof Systems 

      Widom, Jennifer; Gries, David; Schneider, Fred B. (Cornell University, 1986-07)
      Most trace-based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two ...
    • A Conversation with Anil Nerode 

      Nerode, Anil; Gries, David (Internet-First University Press, 2014-10-16)
      Anil Nerode is the Goldwin Smith Professor of Mathematics. He joined the Cornell Math Department in 1959. His interests are in mathematical logic, the theory of automata, computability and complexity theory, the calculus ...
    • A Conversation with David Gries 

      Gries, David; Constable, Robert L. (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 Fred Schneider 

      Schneider, Fred B.; Gries, David (Internet-First University Press, 2015-09-09)
      Fred Schneider, an expert in concurrent and distributed systems and in computer and cybersecurity, shares insights about how his professional interests evolved, and provides sweeping views about how his field and department ...
    • A Conversation with John E. Hopcroft 

      Hopcroft, John E.; Gries, David (Internet-First University Press, 2015-07-21)
      This ACM Turing Award recipient talks about research, textbooks, working with graduate students, his role as a senior statesman of his field and concludes with some words of wisdom.
    • A Conversation with Richard W. Conway 

      Conway, Richard W.; Gries, David (Internet-First University Press, 2015-07-21)
      Dick Conway came to Cornell in 1949, as a freshman. He received the first PhD from Operations Research and Industrial Engineering (1958), was instrumental in the creation of the CS Department (1965) and was a founding ...
    • A Conversation with Robert L. Constable 

      Constable, Robert L.; Gries, David (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 ...
    • A Conversation with Tim Teitelbaum 

      Teitelbaum, Tim; Gries, David (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 

      Gries, David (Cornell University, 1976-07)
    • Describing an Algorithm by Hopcroft 

      Gries, David (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 

      Xue, Jinyun; Gries, David (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 ...