Dafny for Metatheory of Programming Languages

Related talk at MSR.

Dafny

Dafny is an open-source automatic program verifier for functional correctness developed at Microsoft Research.

Software Foundations

Software Foundations is a textbook on programming languages written in Coq and available online.

I've translated some parts of Software Foundations from Coq to Dafny.

• Imp
• Types: Type Systems
• Stlc: The Simply Typed Lambda-Calculus
• Norm: Normalization of STLC
• References: Typing Mutable References

Beyond Software Foundations

• StlcLn: Locally-nameless STLC
• LnSystemF: Locally-nameless System F
• DependentTypes: a syntax-directed dependently typed system

Step-Indexed Logical Relations

Step-indexed logical relations seem like a natural fit for Dafny. Hence, I am formalizing Amal Ahmed's Lectures on Logical Relations.

• Lr_Ts_Stlc.dfy: Proof of type-safety of the STLC using step-indexed logical relations.

• Lr_Ts_Stlc_IsoRecTypes.dfy: Augment STLC with iso-recursive types (explicit fold and unfold). The previous proof simply needs to be augmented as well. The old cases remain unchanged.