William L. Lewis Professor of Engineering
Cornell Weiss Presidential Fellow
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.
- 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
- 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
- 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
- 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
- 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
- ____. ACM SIGCSE Conference, Philadelphia, PA, February 17, 1996 (with
- 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
- Equational logic as a tool. Invited lecture. 4th International
Conference, AMAST '95, Montreal, Canada, 3 July 1995.
- 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
- 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).
1995-1996 Annual Report Home Page
Departmental Home Page
If you have questions or comments please contact:
Last modified: 2 November 1996 by Denise Moore