Type inference verified: Algorithm W in Isabelle/HOL

This publication has 15 references indexed in Scilit:

• Pure type systems formalized
  Published by Springer Nature ,2005
• A theory of type polymorphism in programming
  Published by Elsevier ,2003
• Compiler verification in LF
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
• Type Reconstruction for Type Classes
  Journal of Functional Programming, 1995
• Functional unification of higher-order patterns
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,1993
• Verifying the unification algorithm in LCF
  Science of Computer Programming, 1985
• Principal type-schemes for functional programs
  Published by Association for Computing Machinery (ACM) ,1982
• HOPE
  Published by Association for Computing Machinery (ACM) ,1980
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem
  Indagationes Mathematicae, 1972
• The Principal Type-Scheme of an Object in Combinatory Logic
  Transactions of the American Mathematical Society, 1969