Principles of Programming Seminar

Wednesday, September 21, 2016 - 4:00pm


Reddy Conference Room 4405 Gates & Hillman Centers


BOHUA ZHAN, NSF Postdoctoral Fellow

AUTO2 is a new heuristic theorem prover written for the proof assistant Isabelle. It uses a robust search mechanism that bears some similarity to those used in SMT solvers. On the other hand, it retains several advantages of the tactics framework in Isabelle, such as allowing custom procedures and working with higher-order logic. In this talk, I will discuss the ideas behind auto2 and show some examples of its use in various parts of mathematics and computer science. In the end I will also discuss the more recent application to automation in separation logic.

Bohua Zhan is a postdoc in the department of mathematics at MIT, currently working on automation techniques in interactive theorem provers. Previously I worked in low-dimensional topology, receiving my PhD in mathematics from Princeton, under the supervision of Zoltan Szabo.
Faculty Host: Jeremy Avigad

Event Website:

For More Information, Contact:


Seminar Series