CS303 Types in Programming Languages: Supplemental Readings

• Type checking algorithm for the simply-typed lambda calculus
• Philip Wadler, Proofs are Programs: 19th Century Logic and 21st Century Computing , 2000
• Classical Logic in a Judgemental Style , natural deduction presentation of FOL
• Jonathan Eifrig and Scott Smith and Valery Trifonov, Type Inference for Recursively Constrained Types and its Application to OOP, 1995
• Valery Trifinov and Scott Smith, Subtyping Constrained Types, 1996
• Christian Skalka and François Pottier, Syntactic Type Soundness for HM(X), 2003