Dafny for Metatheory of Programming Languages
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
HSubst.dfy
HSubstD.dfy
Imp.dfy
LnSystemF.dfy
Lr_Ts_Stlc.dfy
Lr_Ts_Stlc_IsoRecTypes.dfy
Lr_Ts_Stlc_MutRefs.dfy
NominalSystemF.dfy
Norm.dfy
README.md
References.dfy
Siek.dfy
Stlc.dfy
StlcLn.dfy
SystemF.dfy
Types.dfy

README.md

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.

Beyond Software Foundations

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.