nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Formalization of a Polymorphic Subtyping Algorithm

verfasst von : Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Modern functional programming languages such as Haskell support sophisticated forms of type-inference, even in the presence of higher-order polymorphism. Central to such advanced forms of type-inference is an algorithm for polymorphic subtyping. This paper formalizes an algorithmic specification for polymorphic subtyping in the Abella theorem prover. The algorithmic specification is shown to be decidable, and sound and complete with respect to Odersky and Läufer’s well-known declarative formulation of polymorphic subtyping.

While the meta-theoretical results are not new, as far as we know our work is the first to mechanically formalize them. Moreover, our algorithm differs from those currently in the literature by using a novel approach based on worklist judgements. Worklist judgements simplify the propagation of information required by the unification process during subtyping. Furthermore they enable a simple formulation of the meta-theoretical properties, which can be easily encoded in theorem provers.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

Nächstes Kapitel An Agda Formalization of Üresin & Dubois’ Asynchronous Fixed-Point Theory

https://github.com/JimmyZJX/Abella-subtyping-algorithm.

Abel, A., Pientka, B.: Higher-order dynamic pattern unification for dependent types and records. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 10–26. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21691-6_5CrossRefMATH

Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008 (2008)

Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: The 18th International Conference on Theorem Proving in Higher Order Logics (2005)

Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008 (2008)

Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1982 (1982)

Disciple Development Team: The Disciplined Disciple Compiler (2017). http://disciple.ouroborus.net/

Dubois, C.: Proving ML type soundness within Coq. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 126–144. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44659-1_9CrossRef

Dubois, C., Menissier-Morain, V.: Certification of a type inference tool for ML: Damas-Milner within Coq. J. Autom. Reasoning 23(3), 319–346 (1999)MathSciNetCrossRef

Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 (2013)

10.

Gacek, A.: The abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_13CrossRef

11.

Garrigue, J.: A certified implementation of ML with structural polymorphism and recursive types. Mathe. Struct. Comput. Sci. 25(4), 867–891 (2015)MathSciNetCrossRef

12.

Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, FPCA 1993 (1993)

13.

Gundry, A., McBride, C., McKinna, J.: Type inference in context. In: Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP 2010 (2010)

14.

Hindley, R.: The principal type-scheme of an object in combinatory logic. Trans. Am. Mathe. Soc. 146, 29–60 (1969)MathSciNetMATH

15.

Jones, M.P.: Functional programming with overloading and higher-order polymorphism. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 97–136. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-59451-5_4CrossRef

16.

Peyton Jones, S., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. J. Funct. Program. 17(1), 1–82 (2007)MathSciNetCrossRef

17.

Lämmel, R., Jones, S.P.: Scrap your boilerplate: a practical design pattern for generic programming. In: Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI 2003 (2003)

18.

Launchbury, J., Peyton Jones, S.L.: State in Haskell. LISP Symbolic Comput. 8(4), 293–341 (1995)CrossRef

19.

Le Botlan, D., Rémy, D.: MLF: raising ML to the power of system F. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003 (2003)

20.

Leijen, D.: HMF: Simple type inference for first-class polymorphism. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008 (2008)

21.

Leroy, X., et al.: The CompCert verified compiler. Documentation and user’s manual, INRIA Paris-Rocquencourt (2012)

22.

Miller, D.: Abstract syntax for variable binders: an overview. In: Lloyd, J., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 239–253. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44957-4_16CrossRef

23.

Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978)MathSciNetCrossRef

24.

Naraschewski, W., Nipkow, T.: Type inference verified: algorithm W in Isabelle/HOL. J. Autom. Reason. 23(3), 299–318 (1999)MathSciNetCrossRef

25.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higherorderlogic, vol. 2283. Springer Science & Business Media, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

26.

Odersky, M., Läufer, K.: Putting type annotations to work. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1996 (1996)

27.

Reed, J.: Higher-order constraint simplification in dependent type theory. In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 (2009)

28.

Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing, pp. 513–523 (1983)

29.

The Coq development team: The Coq proof assistant (2017). https://coq.inria.fr/

30.

The PureScript development team: PureScript (2017). http://www.purescript.org/

31.

Tiuryn, J., Urzyczyn, P.: The subtyping problem for second-order types is undecidable. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science (1996)

32.

Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)MathSciNetCrossRef

33.

Urban, C., Nipkow, T.: Nominal verification of algorithm W. from semantics to computer science. In: Essays in Honour of Gilles Kahn, pp. 363–382 (2008)

34.

Vytiniotis, D., Weirich, S., Peyton Jones, S.: FPH: first-class polymorphism for Haskell. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008 (2008)

35.

Wells, J.B.: Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98(1–3), 111–156 (1999)MathSciNetCrossRef

Titel: Formalization of a Polymorphic Subtyping Algorithm
verfasst von: Jinxu Zhao
Bruno C. d. S. Oliveira
Tom Schrijvers
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_36

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner