Progressive Types

Joe Gibbs Politz, Hannah Quay-de la Vallee, and Shriram Krishnamurthi

@inproceedings{politz:progressive-types,
  author = {Joe Gibbs Politz and Hannah Quay-de la Vallee and Shriram Krishnamurthi},
  title = {{Progressive Types}},
  year = 2012,
  booktitle = {{SPLASH/Onward!}}
}
  

The paper. (pdf)

Update 13 May 2013: Updated versions of the proofs presented in the paper: (pdf). The link below is included for reference. We fixed bugs in the Application and Substitution Lemmas.

Original proofs for the type system presented in the paper. (pdf)

The Redex model and mechanized proofs in Coq. (github).