Certifying Dictionary Construction in Isabelle/HOL

• Autorzy: Hupel Lars

Identyfikatory

DOI

10.3233/FI-2019-1859

• Języki publikacji: EN

Abstrakty

EN

Type classes are a well-known extension to various type systems. Classes usually participate in type inference; that is, the type checker will automatically deduce class constraints and select appropriate instances. Compilers for such languages face the challenge that concrete instances are generally not directly mentioned in the source text. In the runtime, type class operations need to be packaged into dictionaries that are passed around as pointers. This article presents the most common approach for compilation of type classes – the dictionary construction – carried out in a trustworthy fashion in Isabelle/HOL, a proof assistant. The result is an automatic routine that eliminates occurences of classes and instances from a set of definitions and proves a theorem relating old and new definitions.

Słowa kluczowe

EN

Isabelle; HOL; type systems; type classes; interactive theorem proving; dictionary construction

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 177--205
• Opis fizyczny: Bibliogr. 44 poz., rys.

Twórcy

autor

Hupel Lars

• Technische Universität München, Fakultät für Informatik, Boltzmannstrasse 3, 85748 Garching, Germany

Bibliografia

• [1] Nipkow T, Klein G. Concrete Semantics. Springer, 2014. ISBN 3319105418. URL http://www.concrete-semantics.org/.
• [2] Haftmann F, Nipkow T. Code Generation via Higher-Order Rewrite Systems. In: Blume M, Kobayashi N, Vidal G (eds.), Functional and Logic Programming: 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-12251-4, 2010 pp. 103-117. doi:10.1007/978-3-642-12251-4_9.
• [3] Haftmann F, Wenzel M. Constructive Type Classes in Isabelle. In: Altenkirch T, McBride C (eds.), Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-74464-1, 2007 pp. 160-174. doi:10.1007/978-3-540-74464-1_11.
• [4] Wenzel M. Type classes and overloading in higher-order logic. In: Gunter EL, Felty A (eds.), Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs ’97 Murray Hill, NJ, USA, August 19-22, 1997 Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-69526-4, 1997 pp. 307-322. doi:10.1007/BFb0028402.
• [5] Hupel L. Dictionary Construction. Archive of Formal Proofs, 2017. http://isa-afp.org/entries/Dict_Construction.html, Formal proof development.
• [6] Hupel L, Nipkow T. A Verified Compiler from Isabelle/HOL to CakeML. In: Ahmed A (ed.), Programming Languages and Systems. Springer International Publishing, Cham. ISBN 978-3-319-89884-1, 2018 pp. 999-1026.
• [7] Kumar R, Myreen MO, Norrish M, Owens S. CakeML: A Verified Implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, New York, NY, USA. ISBN 978-1-4503-2544-8, 2014 pp. 179-191. doi:10.1145/2535838.2535841.
• [8] Krauss A. Partial and Nested Recursive Function Definitions in Higher-order Logic. Journal of Automated Reasoning, 2010. 44(4):303-336. doi:10.1007/s10817-009-9157-2.
• [9] Krauss A. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Dissertation, Technische Universitt Mnchen, Mnchen, 2009.
• [10] Blanchette JC, Hlzl J, Lochbihler A, Panny L, Popescu A, Traytel D. Truly Modular (Co)datatypes for Isabelle/HOL. In: Interactive Theorem Proving. Springer International Publishing, 2014 pp. 93-110. doi:10.1007/978-3-319-08970-6_7.
• [11] Morris JG. Type Classes and Instance Chains: A Relational Approach. Ph.D. thesis, Portland State University, 2013. URL http://homepages.inf.ed.ac.uk/jmorri14/pubs/morris-dissertation.pdf.
• [12] Peterson J, Jones M. Implementing Type Classes. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93. ACM, New York, NY, USA. ISBN 0-89791-598-4, 1993 pp. 227-236. doi:10.1145/155090.155112.
• [13] Augustsson L. Implementing Haskell Overloading. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, FPCA ’93. ACM, New York, NY, USA. ISBN 0-89791-595-X, 1993 pp. 65-73. doi:10.1145/165180.165191.
• [14] Chen K, Hudak P, Odersky M. Parametric Type Classes. In: Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP ’92. ACM, New York, NY, USA. ISBN 0-89791-481-3, 1992 pp. 170-181. doi:10.1145/141471.141536.
• [15] Lämmel R, Jones SP. Scrap Your Boilerplate with Class: Extensible Generic Functions. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, ICFP ’05. ACM, New York, NY, USA. ISBN 1-59593-064-7, 2005 pp. 204-215. doi:10.1145/1086365.1086391.
• [16] Meng J, Paulson LC. Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning, 2007. 40(1):35-60. doi:10.1007/s10817-007-9085-y.
• [17] Blanchette JC, Bulwahn L, Nipkow T. Automatic Proof and Disproof in Isabelle/HOL. In: Frontiers of Combining Systems. Springer, 2011 pp. 12-27.
• [18] Blanchette JC. Automatic Proofs and Refutations for Higher-Order Logic. Dissertation, Technische Universitt Mnchen, Mnchen, 2012.
• [19] Brady E. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 2013. 23(05):552-593. doi:10.1017/s095679681300018x.
• [20] Sozeau M, Oury N. First-Class Type Classes. In: Lecture Notes in Computer Science, pp. 278-293. Springer Berlin Heidelberg, 2008. doi:10.1007/978-3-540-71067-7_23.
• [21] Oliveira BC, Moors A, Odersky M. Type Classes As Objects and Implicits. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’10. ACM, New York, NY, USA. ISBN 978-1-4503-0203-6, 2010 pp. 341-360. doi:10.1145/1869459.1869489.
• [22] Hall CV, Hammond K, Jones SLP, Wadler PL. Type classes in Haskell. ACM Transactions on Programming Languages and Systems, 1996. 18(2):109-138. doi:10.1145/227699.227700.
• [23] Naraschewski W, Wenzel M. Object-oriented verification based on record subtyping in Higher-Order Logic. In: Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1998 pp. 349-366. doi:10.1007/bfb0055146.
• [24] Milner R. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1978. 17(3):348-375. doi:10.1016/0022-0000(78)90014-4.
• [25] Hindley JR. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society, 1969. 146:29. doi:10.2307/1995158.
• [26] Jones MP. Qualified Types: Theory and Practice. Cambridge University Press, 1994. ISBN 9780511663086. doi:10.1017/cbo9780511663086.
• [27] Nipkow T, Snelting G. Type classes and overloading resolution via order-sorted unification. In: Functional Programming Languages and Computer Architecture. Springer Berlin Heidelberg, 1991 pp. 1-14. doi:10.1007/3540543961_1.
• [28] Nipkow T, Prehofer C. Type Reconstruction for Type Classes. Journal of Functional Programming, 1995. 5(2):201-224. doi:10.1017/S0956796800001325.
• [29] Reynolds JC. Types, Abstraction and Parametric Polymorphism. In: IFIP Congress. 1983 pp. 513-523.
• [30] Lochbihler A. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. In: Thiemann P (ed.), Programming Languages and Systems (ESOP 2016), volume 9632 of LNCS. Springer, 2016 pp. 503-531. doi:10.1007/978-3-662-49498-1_20.
• [31] Gilcher J, Lochbihler A, Traytel D. Conditional Parametricity in Isabelle/HOL, 2017. Extended abstract, URL https://people.inf.ethz.ch/trayteld/papers/itp17poster-cond_param/cond.pdf.
• [32] Blanchette JC, Popescu A, Traytel D. Operations on Bounded Natural Functors. Archive of Formal Proofs, 2017. http://isa-afp.org/entries/BNF_Operations.html, Formal proof development.
• [33] Gordon AD, Fournet C. Principles and Applications of Refinement Types. NATO Science for Peace and Security Series - D: Information and Communication Security, 2010. 25(Logics and Languages for Reliability and Security):73-104. doi:10.3233/978-1-60750-100-8-73.
• [34] Finn S, Fourman MP, Longley J. Partial Functions in a Total Setting. Journal of Automated Reasoning, 1997. 18(1):85-104. doi:10.1023/a:1005702928286.
• [35] Wimmer S, Hu S, Nipkow T. Verified Memoization and Dynamic Programming. In: Interactive Theorem Proving, pp. 579-596. Springer International Publishing, 2018. doi:10.1007/978-3-319-94821-8_34.
• [36] Myreen MO, Owens S. Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming, 2014. 24(2-3):284-315. doi:10.1017/S0956796813000282.
• [37] Felty A. A logic programming approach to implementing higher-Order term rewriting. In: Eriksson LH, Hallnäs L, Schroeder-Heister P (eds.), Extensions of Logic Programming, pp. 135-161. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-47114-1, 1992. doi:10.1007/BFb0013606.
• [38] Felty A. Higher-Order Conditional Rewriting in the L-lambda Logic Programming Language, 1992. URL http://www.site.uottawa.ca/~afelty/dist/welp92a.pdf.
• [39] Slind K. Reasoning about Terminating Functional Programs. Ph.D. thesis, Technische Universitt Mnchen, 1999. URL http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss1999111516455.
• [40] Sternagel C, Thiemann R. Haskell’s Show Class in Isabelle/HOL. Archive of Formal Proofs, 2014. http://isa-afp.org/entries/Show.html, Formal proof development.
• [41] Hughes J. A novel representation of lists and its application to the function “reverse”. Information Processing Letters, 1986. 22(3):141-144. doi:10.1016/0020-0190(86)90059-1.
• [42] Haftmann F, Krauss A, Kunčar O, Nipkow T. Data Refinement in Isabelle/HOL. In: Blazy S, Paulin-Mohring C, Pichardie D (eds.), Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science. 2013 pp. 100-115.
• [43] Manna Z, Pnueli A. Formalization of Properties of Functional Programs. Journal of the ACM, 1970. 17(3):555-569. doi:10.1145/321592.321606.
• [44] Hurd J. The Open Theory Standard Theory Library. In: Bobaru M, Havelund K, Holzmann GJ, Joshi R (eds.), NASA Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-20398-5, 2011 pp. 177-191.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).