A higher-order abstract syntax approach to verified transformations on functional programs. (English) Zbl 1335.68036
Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 752-779 (2016).
Summary: We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language \(\lambda\)Prolog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations that analyze binding structure. We do this by describing concise encodings in \(\lambda\)Prolog for transformations like typed closure conversion and code hoisting that are sensitive to such structure and by showing how to prove their correctness using Abella.
For the entire collection see [Zbl 1333.68019].
For the entire collection see [Zbl 1333.68019].
References:
| [1] | Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69–83. Springer, Heidelberg (2006) · Zbl 1178.68146 · doi:10.1007/11693024_6 |
| [2] | Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001) · doi:10.1145/504709.504712 |
| [3] | Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005) · Zbl 1152.68516 · doi:10.1007/11541868_4 |
| [4] | Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reasoning 7(2), 1–89 (2014) |
| [5] | Baelde, D., Nadathur, G.: Combining deduction modulo and logics of fixed-point definitions. In: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pp. 105–114. IEEE Computer Society (2012) · Zbl 1361.68132 · doi:10.1109/LICS.2012.22 |
| [6] | Bélanger, O.S., Chaudhuri, K.: Automatically deriving schematic theorems for dynamic contexts. In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. ACM Press (2014) · doi:10.1145/2631172.2631181 |
| [7] | Savary-Belanger, O., Monnier, S., Pientka, B.: Programming type-safe transformations using higher-order abstract syntax. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 243–258. Springer, Heidelberg (2013) · Zbl 1426.68061 · doi:10.1007/978-3-319-03545-1_16 |
| [8] | Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004) · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5 |
| [9] | de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae 34(5), 381–392 (1972) · Zbl 0253.68007 · doi:10.1016/1385-7258(72)90034-0 |
| [10] | Cave, A., Pientka, B.: A case study on logical relations using contextual types. In: Proceedings of the Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, EPTCS, vol. 185, pp. 33–45 (2015) · doi:10.4204/EPTCS.185.3 |
| [11] | Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 54–65. ACM Press (2007) · doi:10.1145/1250734.1250742 |
| [12] | Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940) · Zbl 0023.28901 · doi:10.2307/2266170 |
| [13] | Danvy, O., Filinski, A.: Representing control: a study of the CPS transformation. Math. Struct. Comput. Sci. 2, 361–391 (1992) · Zbl 0798.68102 · doi:10.1017/S0960129500001535 |
| [14] | Dargaye, Z.: Vérification formelle d’un compilateur optimisant pour langages fonctionnels. Ph.D. thesis, l’Université Paris 7-Denis Diderot, France (2009) |
| [15] | Gordon, M.J.C.: Introduction to the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, pp. 2–3. IEEE Computer Society (1991) · doi:10.1109/HOL.1991.596265 |
| [16] | Hannan, J., Pfenning, F.: Compiler verification in LF. In: 7th Symposium on Logic in Computer Science. IEEE Computer Society Press (1992) · doi:10.1109/LICS.1992.185552 |
| [17] | Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060 |
| [18] | Hickey, J., Nogin, A.: Formal compiler construction in a logical framework. Higher-Order Symb. Comput. 19(2–3), 197–230 (2006) · Zbl 1105.68020 · doi:10.1007/s10990-006-8746-6 |
| [19] | Hur, C.K., Dreyer, D.: A Kripke logical relation between ML and assembly. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 133–146. ACM Press (2011) · Zbl 1284.68148 · doi:10.1145/1926385.1926402 |
| [20] | Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191. ACM Press (2014) · Zbl 1284.68405 · doi:10.1145/2535838.2535841 |
| [21] | Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42–54. ACM Press (2006) · Zbl 1369.68124 · doi:10.1145/1111037.1111042 |
| [22] | McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol. 19, pp. 33–41. American Mathematical Society (1967) · Zbl 0183.19201 · doi:10.1090/psapm/019/0242403 |
| [23] | McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 91–119 (2000) · Zbl 0951.03050 · doi:10.1016/S0304-3975(99)00171-1 |
| [24] | Miller, D.: Abstract syntax for variable binders: an overview. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 239–253. Springer, Heidelberg (2000) · Zbl 0983.68036 · doi:10.1007/3-540-44957-4_16 |
| [25] | Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012) · Zbl 1267.68014 · doi:10.1017/CBO9781139021326 |
| [26] | Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749–783 (2005) · Zbl 1367.03059 · doi:10.1145/1094622.1094628 |
| [27] | Milner, R., Weyrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 51–72. Edinburgh University Press, Edinburgh (1972) · Zbl 0259.68008 |
| [28] | Minamide, Y., Morrisett, G., Harper, R.: Typed closure conversion. Technical report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University (1995) |
| [29] | Murphy VII, T.: Modal types for mobile code. Ph.D. thesis, Carnegie Mellon University (2008) |
| [30] | Nadathur, G., Miller, D.: An overview of \[ \lambda \] {\(\lambda\)} Prolog. In: Fifth International Logic Programming Conference, pp. 810–827. MIT Press (1988) |
| [31] | Nanevski, A., Pfenning, F., Pientka, B.: Contextual model type theory. ACM Trans. Comput. Logic 9(3), 1–49 (2008) · Zbl 1367.03060 · doi:10.1145/1352582.1352591 |
| [32] | Neis, G., Hur, C.K., Kaiser, J.O., McLaughlin, C., Dreyer, D., Vafeiadis, V.: Pilsner: a compositionally verified compiler for a higher-order imperative language. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp. 166–178. ACM Press (2015) · Zbl 1360.68350 · doi:10.1145/2784731.2784764 |
| [33] | Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [34] | Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15–21. Springer, Heidelberg (2010) · Zbl 1291.68366 · doi:10.1007/978-3-642-14203-1_2 |
| [35] | Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003) · Zbl 1056.03014 · doi:10.1016/S0890-5401(03)00138-X |
| [36] | Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system - Version 2. http://teyjus.cs.umn.edu/ |
| [37] | Tian, Y.H.: Mechanically verifying correctness of CPS compilation. In: Twelfth Computing: The Australasian Theory Symposium. CRPIT, vol. 51, pp. 41–51. ACS (2006) |
| [38] | Tiu, A.: Stratification in logics of definitions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 544–558. Springer, Heidelberg (2012) · Zbl 1358.03031 · doi:10.1007/978-3-642-31365-3_43 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
