I manage the Openproof project where we develop courseware for teaching logic. Our packages include Language, Proof and Logic which has been translated into German, Japanese and Portuguese; Tarski's World which has been in print since the mid 1980s and Hyperproof which will soon be republished in a new edition.Our courseware packages consist of text books, desktop applications and online services, including video lectures available through Stanford Online.As part of this project we analyze learner data to uncover error patterns common to logic learners.I also have an active research program into the logic of diagrammatic representations.

Collaborators have included Jon Barwise, Richard Cox, Robert Dale, John Etchemendy, Mark Greaves, Albert Liu, Michael Murray, Nik Swoboda, Atsushi Shimojima, and many others.

Taught all aspects of the computer science curriculum including AI, automated reasoning, data structures and algorithms, theory of computation, programming language design, and intro computer science.Active research project in collaboration with Sidney Bailin into automated natural deduction in set theory, with work published in the CADE conferences and the Journal of Automated Reasoning.

Investigated the use of HOL as the basis for program verification. Project led by Steve Crocker.

Taught undergraduate course in Artificial Intelligence, and a graduate course in Automated Reasoning.

Worked on research project led by Hassan Ait-Kaci and Roger Nasr on the design of multi-paradigm programming languages. Developed first prototype interpreter for LIFE, a language combining logic, functional and object-oriented paradigms.