My dissertation research at Yale focused on the design, metatheory, implementation and usage of a novel programming language and proof assistant, called VeriML. The goal behind VeriML is to enable scalable development of logical proofs; the main idea about how to achieve this goal is to have good support for writing proof-producing functions with precise, typed signatures.

More precisely, VeriML aims to provide a compelling alternative to tactic development compared to existing approaches, by leveraging a rich type system coupled with a rich ML-style programming model. I have also shown how generalizations of features of traditional proof assistants, such as interactive development of proofs and tactics, are a direct consequence of VeriML’s design. Thus the language can be viewed as a proof assistant in its entirety. Through the addition of a simple staging construct, VeriML provides extensible static checking of proofs and tactics, solving long-standing issues such as having a safe yet user-extensible conversion rule. Because of this support, users are free to extend the ‘background reasoning’ that the proof assistant uses to handle trivial details with domain-specific sophistication of arbitrary complexity; this simplifies the development of further proofs and automation, yielding an approach to formal proofs closer to informal practice.




  • VeriML version 0.5. A lot of big and small improvements and changes; the most major ones being that VeriML is now compiled through translation to ML (instead of interpreted) and that there is some inductive definition support.
  • VeriML version 0.3. This reflects VeriML as described in our POPL 2012 paper.
  • VeriML version 0.1. An older version corresponding to our ICFP 2010 paper.