Certified theorem proving (Nuprl in Coq)
Allen's Partial Equivalence Relation (PER) semantics provides a semantics for Nuprl's type theory that allows one to prove that Nuprl's inference rules are valid, and therefore that Nuprl is consistent. Until our ITP 2014 paper, these proofs were done by hand. In order to formally prove that these rules are correct (and therefore that Nuprl is consistent), we have implemented this PER semantics using the Coq proof assistant. This implementation (1) provides a bridge between Nuprl and Coq, and (2) is the basis for developing certified versions of Nuprl. This is joint work with Abhishek Anand and Mark Bickford.
Certified theorem proving (KeYmaera X in Coq)
KeYmaera X is a theorem prover for cyber-physical systems (modeled as hybrid systems) that implements a logic called Differential Dynamic Logic (dL for short). KeYmaera X has a small core thanks a uniform substitution based proof calculus. We have implemented and verified this core in Coq. Check out our implementation for details. This was joint work with Brandon Bohrer and Andre Platzer from CMU, who have implemented and verified KeYmaera's core in Isabelle.
Intuitionistic and Nominal Type Theory
Using our formalization of Nuprl in Coq, we are turning Nuprl into an intuitionistic type theory, i.e., we have proved that some versions of Brouwer's continuity and bar induction principles are valid w.r.t. Nuprl's PER semantics. In order to prove the validity of such continuity principles we have turned Nuprl into a nominal type theory. It remains open whether stronger continuity and bar induction rules are also valid.
EventML is a ML-like constructive specification language that implements a paradigm for verified programming. It gives precedence to the programming task, and also allows programmers to cooperate with a proof assistant in order to structure arguments of correctness. It is designed specifically to cooperate with the Nuprl proof assistant in order to develop correct-by-construction asynchronous protocols.
Synthesis and verification of distributed protocols
Using EventML, we have specified, synthesized, and verified safety properties of the Multi-Paxos protocol. To do so, we have automated some patterns of reasoning; and to get efficient code, we have built a process optimizer in Nuprl. We are reusing this methodology to develop other provably correct protocols, striving towards more resilient and trustworthy systems. One of our current goal is to verify Byzantine fault tolerant protocols written in C using, among other things, the Verified Software Toolchain (VST).
Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. Skalpel implements a promising approach to making type errors easier to understand and fix called type error slicing, in which slices (program points) containing all and only the information needed by the programmer to understand and fix a type error are identified and exhibited. Check out the web page of our project, from which you can download packages for Debian and Red-Hat-based systems as well as a web demo.
Semantics of expansion
Intersection types introduce type polymorphism in a finitary way. Expansion was introduced to recover the principal typing property in such systems. The study of realisability semantics for such systems with expansion might help casting some light on the expansion mechanism.
Reducibility is a method based on realisability semantics where the idea is to interpret types by sets of λ-terms closed under some properties. This method seems promising in generalising diverse properties' proofs of the (typed or untyped) λ-calculus.