David Gries

David Gries
William L. Lewis Professor of Engineering
Cornell Weiss Presidential Fellow
http://www.cs.cornell.edu/home/gries/gries.html
Dr. rer. nat., Munich Institute of Technology, 1966

My research is aimed at gaining a better understanding of the programming process, with respect to both sequential and concurrent (or parallel) programs. The work requires investigation of theories of program correctness and their application, as well as investigation of other concepts in the semantics of programming languages. A procedural programming language, Polya, is being defined and implemented. We are attempting to make the language in which algorithms are usually presented the programming language, but without loss of efficiency. This has entailed work in the theory of polymorphic types and type inference as well as the development of new constructs for defining types and for describing the implementation of variables. The hope is that this work will advance the state of the art of reusability of program parts and will raise the level at which programs are written.

Education, in particular the material taught in the first few courses in computer science, is of particular interest. A text for a discrete mathematics course, co-authored with F.B. Schneider, has been published. It emphasizes the pervasive use of an equational logic and formal calculation in discrete math-ematics. Research continues on equational logic and its applications.

Awards

Cornell Weiss Presidential Fellow
1995 ACM Karl V. Karlstrom Outstanding Educator Award
Honorary Doctor of Laws, Daniel Webster College, Nashua, NH
Faculty of the Year, Cornell Association for Computer Science Undergraduates

University Activities

Cornell University Faculty Senate
General Committee of the Graduate School
Engineering Policy Committee
Engineering Faculty Development Committee
Graduate School Fellowship-folder review committee
Weiss Award Committee

Professional Activities

Managing Editor: Information Processing Letters
Main Editor: Acta Informatica
Editor: Springer-Verlag Texts and Monographs in Computer Science
Editorial Board: Springer-Verlag Lecture Notes in Computer Science, Software-Concepts and Tools, Formal Aspects of Computer Science
Program committee: Third International Conference on the Mathematics of Program Construction; IFIP TC2 Working Conference on Algorithmic Languages and Calculi; ENCRES 1997
Co-organizer: DIMACS Workshop on teaching logic, Rutgers, July 1996
Director: Marktoberdorf summer school, 1996
IFIP Working Group 2.3 (Programming Methodology)
Referee/Reviewer: Communications of the ACM; IEEE Transactions in Software Engineering; IEEE Computer; Science of Computer Programming; Information Processing Letters; NSF

Lectures

Speaking documents-T.V. Raman's system AsTeR. Engineering Council Conference, Cornell University, Ithaca, NY, 12 April 1996.
Formal methods: Why? what? how? One-day tutorial. SEI Conference on Software Engineering Education, Daytona Beach, FL, 21 April 1996 (with Neville Dean).
____. ACM SIGCSE Conference, Philadelphia, PA, February 17, 1996 (with Neville Dean).
Calculational logic: A useful tool. The Bill Sears Club, Center for Applied Mathematics, Cornell University, Ithaca, NY, 3 October 1995.
On using insight from formal methods and programming methodology to present algorithms. Invited lecture. Carleton Algorithms Theory Symposium, Carleton University, Ottawa, Canada, 30 September 1995.
Equational logic: A great pedagogical tool for teaching a skill in logic. Education Day, ZUM '95, Limerick, Ireland, 9 September 1995.
Teaching logic as a tool. One-day tutorial, ZUM '95. Limerick, Ireland, 7 September 1995.
The consequences of teaching proof to mathematics students using the calculational approach to logic. Invited lecture. Irish Mathematics Society, Limerick, Ireland, 7 September 1995.
A Glimmer(ick) of hope. ZUM '95. Banquet speech. Limerick, Ireland, 7 September 1995.
Equational logic as a tool. Invited lecture. 4th International Conference, AMAST '95, Montreal, Canada, 3 July 1995.

Publications

Interactive audio documents. Journal of Visual Languages and Computing 7 (1996), 97-108 (with T.V. Raman).
The need for education in useful formal logic. IEEE Computer (April 1996), 29-30.
Avoiding the undefined by underspecification. In J. van Leeuwen (Ed.), Computer Science Today. LNCS 1000, Springer-Verlag, October 1995, 366-373 (with F.B. Schneider).
Teaching math more effectively through calculational proofs. The Mathematical Monthly (October 1995), 691-697 (with F.B. Schneider).
Equational logic as a tool. Algebraic Methodology and Software Technology. LNCS 936, July 1995, 1-17.
Teaching about proof. Arts & Sciences Newsletter. Cornell University, Spring 1995, p. 3 (with F.B. Schneider).

Return to: