Date: Wed, 20 Nov 1996 23:00:46 GMT Server: NCSA/1.5 Content-type: text/html Last-modified: Wed, 23 Mar 1994 00:46:34 GMT Content-length: 2490 Harry R. Lewis

Harry Lewis

Gordon McKay Professor of Computer Science

THEORY OF COMPUTATION AND COMPUTER SYSTEMS

Theoretical computer science has its roots in mathematical logic. In the 1930s, using mathematical automata, Turing investigated whether the truth of mathematical propositions could be determined by algorithmic procedures; since then, studies of formalized computers and formalized mathematical systems have continued to complement and enrich one another.

Professor Lewis has worked extensively on the algorithmic solvability of logical, computational, and combinatorial systems, attempting to clarify the relations between them and to identify their common characteristics. For example, he has applied automata theory to the classical predicate calculus and to circuit models for parallel computers.

Currently he is working on practical formal methods for design verification of asynchronous systems, such as boolean circuits and signalling protocols. Timing characteristics of such systems are notoriously difficult to validate under realistic models of their behavior, and most practical computer-aided design tools rely on inexhaustive simulation rather than complete verification. Professor Lewis has developed both a theoretical logical framework for the timing specification of asynchronous systems, and software that uses this specification language to verify the functionality of asynchronous boolean circuits whose components have specified minimum and maximum time delays.

Professor Lewis is actively involved in the use of computers in education, and his books have had a significant influence on the teaching of the foundations of computer science to undergraduates.