Aquinas Hobor
Affiliated Projects
Concurrent C minor: Connecting machine-verified source programs in concurrent programming languages to machine code via machine-verified optimizing compilers. (PDF: project vision, by Andrew W. Appel)
Mechanized Semantic Library: Mechanically-verified mathematical techniques for developing semantic models of program logics and type systems.