A Mechanized Proof of a Textbook Type Unification Algorithm

André Rauber Du Bois, Rodrigo Ribeiro, Maycon Amaro

Abstract


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.


Keywords


Type inference; unification; Coq proof assistant

Full Text:

PDF

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.




DOI: https://doi.org/10.22456/2175-2745.100968

Copyright (c) 2020 Rodrigo Ribeiro, Maycon Amaro, André Rauber Du Bois

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Indexing databases:
        

Acknowledgments: