A Mechanized Proof of a Textbook Type Unification Algorithm
DOI:
https://doi.org/10.22456/2175-2745.100968Keywords:
Type inference, unification, Coq proof assistantAbstract
Unification is the core of type inference algorithms for modern functional programming languages, like Haskell and SML. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks. We also report on the use of such formalization to build a correct type inference algorithm for the simply typed λ-calculus.
Downloads
References
[1] JONES, S. P. Haskell 98 Language and Libraries: the Revised Report. [S.l.: s.n.], 2003.
MILNER, R.; TOFTE, M.; HARPER, R. The Definition of Standard ML. [S.l.]: MIT Press, 1990. I-XI, 1-101 p.
MILNER, R. A Theory of Type Polymorphism in Programming. J. Comput. Syst. Sci., v. 17, n. 3, p. 348–375, 1978.
POTTIER, F.; RÉMY, D. The Essence of ML Type Inference. In: PIERCE, B. C. (Ed.). Advanced Topics in Types and Programming Languages. MIT Press, 2005. cap. 10, p. 389–489. Disponível em: http://cristal.inria.fr/attapl/.
ROBINSON, J. A. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, v. 12, n. 1, p. 23–41, 1965.
BERTOT, Y.; CASTÉRAN, P. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. [S.l.]: Springer Verlag, 2004. (Texts in Theoretical Computer Science).
BOVE, A.; DYBJER, P.; NORELL, U. A Brief Overview of Agda — A Functional Language with Dependent Types. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. Berlin, Heidelberg: Springer-Verlag, 2009. (TPHOLs ’09), p. 73–78.
PAULSON, L. C. Verifying the Unification Algorithm in LCF. CoRR, cs.LO/9301101, 1993.
BOVE, A. Programming in Martin-Löf Type Theory: Unification - A non-trivial Example. 1999. Licentiate Thesis of the Department of Computer Science, Chalmers University of Technology.
MCBRIDE, C. First-order unification by structural recursion. J. Funct. Program., v. 13, n. 6, p. 1061–1075, 2003.
KOTHARI, S.; CALDWELL, J. A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints. In: FERNANDEZ, M. (Ed.). Proceedings 24th International Workshop on Unification. [S.l.: s.n.], 2010. (EPTCS, v. 42), p. 24–38.
MITCHELL, J. C. Foundations of Programming Languages. Cambridge, MA, USA: MIT Press, 1996.
PIERCE, B. C. Types and programming languages. Cambridge, MA, USA: MIT Press, 2002.
MCBRIDE, C.; MCKINNA, J. The view from the left. J. Funct. Program., v. 14, n. 1, p. 69–111, 2004.
LEROY, X. Formal verification of a realistic compiler. Commun. ACM, v. 52, n. 7, p. 107–115, 2009.
BARTHE, G. et al. A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. In: CORTESI, A. (Ed.). VMCAI. [S.l.]: Springer, 2002. (Lecture Notes in Computer Science, v. 2294), p. 32–45.
GONTHIER, G. The Four Colour Theorem: Engineering of a Formal Proof. In: KAPUR, D. (Ed.). ASCM. [S.l.]: Springer, 2007. (Lecture Notes in Computer Science, v. 5081), p. 333.
GONTHIER, G. Engineering mathematics: the odd order theorem proof. In: GIACOBAZZI, R.; COUSOT, R. (Ed.). POPL. [S.l.]: ACM, 2013. p. 1–2.
RIBEIRO, R.; CAMARÃO, C. A mechanized textbook proof of a type unification algorithm. In: SBMF. [S.l.]: Springer, 2015. p. 127–141.
RIBEIRO, R. et al. A Mechanized Textbook Proof of a Type Unification Algorithm — On-line repository. 2015. Https://github.com/rodrigogribeiro/unification.
SØRENSEN, M.; URZYCZYN, P. Lectures on the Curry-Howard Isomorphism. [S.l.]: Elsevier, 2006. (Studies in Logic and the Foundations of Mathematics, v. 10).
CHLIPALA, A. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. Disponível em: http://mitpress.mit.edu/books/certified-programming-dependent-types.
LETOUZEY, P. A New Extraction for Coq. In: Proceedings of the 2002 International Conference on Types for Proofs and Programs. Berlin, Heidelberg: Springer-Verlag, 2003. (TYPES’02), p. 200–219. Disponível em: http://dl.acm.org/citation.cfm?id=1762639.1762651.
SWIERSTRA, W. Xmonad in Coq (Experience Report): Programming a Window Manager in a Proof Assistant. SIGPLAN Not., ACM, New York, NY, USA, v. 47, n. 12, p. 131–136, set. 2012. Disponível em: http://doi.acm.org/10.1145/2430532.2364523.
AYDEMIR, B. E. et al. Engineering formal metatheory. In: NECULA, G. C.; WADLER, P. (Ed.). POPL. [S.l.]: ACM, 2008. p. 3–15.
CHLIPALA, A. Parametric higher-order abstract syntax for mechanized semantics. SIGPLAN Not., ACM, New York, NY, USA, v. 43, n. 9, p. 143–156, set. 2008. Disponível em: http://doi.acm.org/10.1145/1411203.1411226.
HINDLEY, J. R.; SELDIN, J. P. Lambda-Calculus and Combinators: An Introduction. 2. ed. New York, NY, USA: Cambridge University Press, 2008.
Coq Developement Team. Coq Proof Assistant — Reference Manual. 2014. Disponível em: http://coq.inria.fr/distrib/current/refman/.
PIERCE, B. C. et al. Software Foundations. [S.l.]: Electronic textbook, 2015.
CLAESSEN, K.; HUGHES, J. Quickcheck: a lightweight tool for random testing of haskell programs. In: ICFP ’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM, 2000. p. 268–279. Disponível em: http://dx.doi.org/10.1145/351240.351266.
NORDSTRÖM, B. Terminating General Recursion. BIT Numerical Mathematics, v. 28, n. 3, p. 605–619, 1988.
MCBRIDE, C. First-order unification by structural recursion — Correctness proof. Disponível em: http://strictlypositive.org/foubsr-website/proof.ps.
NARASCHEWSKI, W.; NIPKOW, T. Type Inference Verified: Algorithm W in Isabelle/HOL. J. Autom. Reason., Springer-Verlag New York, Inc., Secaucus, NJ, USA, v. 23, n. 3, p. 299–318, nov. 1999. Disponível em: http://dx.doi.org/10.1023/A:1006277616879.
AVELAR, A. B. et al. Verification of the Completeness of Unification Algorithms à la Robinson. In: DAWAR, A.; QUEIROZ, R. J. G. B. de (Ed.). Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings. Springer, 2010. (Lecture Notes in Computer Science, v. 6188), p. 110–124. Disponível em: http://dx.doi.org/10.1007/978-3-642-13824-9_10.
AVELAR, A. B. et al. First-order unification in the PVS proof assistant. Logic Journal of the IGPL, v. 22, n. 5, p. 758–789, 2014. Disponível em: http://dx.doi.org/10.1093/jigpal/jzu012.
DUBOIS, C.; MÉNISSIER-MORAIN, V. Certification of a Type Inference Tool for ML: Damas-Milner within Coq. J. Autom. Reasoning, v. 23, n. 3-4, p. 319–346, 1999. Disponível em: http://dx.doi.org/10.1023/A:1006285817788.
NARASCHEWSKI, W.; NIPKOW, T. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, v. 23, p. 299–318, 1999.
NAZARETH, D.; NIPKOW, T. Formal Verification of Algorithm W: The Monomorphic Case. In: WRIGHT, J. Von; GRUNDY, J.; HARRISON, J. (Ed.). Theorem Proving in Higher Order Logics (TPHOLs’96). Springer, 1996. (LNCS, v. 1125), p. 331–346. Disponível em: http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.dvi.gz.
URBAN, C.; NIPKOW, T. Nominal verification of algorithm W. In: HUET, G.; LÉVY, J.-J.; PLOTKIN, G. (Ed.). From Semantics to Computer Science. Essays in Honour of Gilles Kahn. [S.l.]: Cambridge University Press, 2009. p. 363–382.
GARRIGUE, J. A certified implementation of ML with structural polymorphism. In: UEDA, K. (Ed.). Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings. Springer, 2010. (Lecture Notes in Computer Science, v. 6461), p. 360–375. Disponível em: http://dx.doi.org/10.1007/978-3-642-17164-2_25.
GARRIGUE, J. A certified implementation of ML with structural polymorphism and recursive types. Mathematical Structures in Computer Science, v. 25, n. 4, p. 867–891, 2015. Disponível em: http://dx.doi.org/10.1017/S0960129513000066.
CHARGUÉRAUD, A. The Locally Nameless Representation. J. Autom. Reasoning, v. 49, n. 3, p. 363–408, 2012. Disponível em: http://dblp.unitrier.de/db/journals/jar/jar49.html#Chargueraud12.
RIBEIRO, R.; BOIS, A. D. Certified Bit-Coded Regular Expression Parsing. Proceedings of the 21st Brazilian Symposium on Programming Languages - SBLP 2017, p. 1–8, 2017. Disponível em: http://dl.acm.org/citation.cfm?doid=3125374.3125381.
DOCZKAL, C.; KAISER, J. O.; SMOLKA, G. A constructive theory of regular languages in Coq. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), v. 8307 LNCS, p. 82–97, 2013.