Lambda the Ultimate

Gary T. Leavens is a professor and chair of Computer Science at
the University of Central Florida,
where he has been since August 2007.
Previously he was a professor of computer science at Iowa State
University in Ames, Iowa, where he started in January 1989.
He also received his Ph.D. from MIT in 1989.
Before his graduate studies at MIT, he worked at Bell Telephone
Laboratories in Denver Colorado as a member of technical staff.
Professor Leavens's research interests include programming and
specification language design and semantics, program verification, and
formal methods, with an emphasis on the object-oriented and
aspect-oriented paradigms. His best known work in the area of formal
methods is related to the JML project, an international effort with
many associated tools (see http://jmlspecs.org). He also worked on the design of the specification languages Larch/Smalltalk (with Yoonsik
Cheon) and Larch/C++ (with Yoonsik and Clyde Ruby). These languages
embody insights from his work on the theory of behavioral subtyping
(with Don Pigozzi and Krishna Kishore Dhara). His best known work on
language design and semantics is on aspect-oriented programming
and multiple dispatch languages (joint with Craig Chambers, Todd Millstein, and Curtis Clifton) such as MultiJava. See http://www.eecs.ucf.edu/~leavens for more information on his research.

Programming and specification language design and semantics,
formal methods (program specification and verification),
aspect-oriented languages, object-oriented languages,
software security, information assurance,
distributed languages, type theory, programming methodology,
software engineering,
computer science education.