×

POPLMark reloaded: mechanizing proofs by logical relations. (English) Zbl 1442.68257

Summary: We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68N15 Theory of programming languages
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Cardelli, L., Curien, P.-L. & Lévy, J.-J. (1991) Explicit substitutions. J. Funct. Program.1(4), 375-416. · Zbl 0941.68542
[2] Abbott, M., Altenkirch, T., Mcbride, C. & Ghani, N. (2005) ∂ for data: Differentiating data structures. Fundamenta Informaticae65(1-2), 1-28. · Zbl 1102.68020
[3] Abel, A. (2008) Normalization for the simply-typed lambda-calculus in Twelf. In Logical Frameworks and Metalanguages (LFM’04), Schürmann, C. (ed). Electronic Notes in Theoretical Computer Science, vol. 199. Elsevier, pp. 3-16. · Zbl 1278.68245
[4] Abel, A. (2010) MiniAgda: Integrating sized and dependent types. In Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR 2010, Edinburgh, UK, 15th July 2010, Bove, A., Komendantskaya, E. & Niqui, M. (eds). EPTCS, vol. 43, pp. 14-28.
[5] Abel, A. & Chapman, J. (2014) Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types. In MSFP. EPTCS, vol. 153, pp. 51-67. · Zbl 1464.68050
[6] Abel, A., Öhman, J. & Vezzosi, A. (2018) Decidability of conversion for type theory in type theory.Proc. ACM Program. Lang.2(POPL), 23:1-23:29.
[7] Abel, A., Pientka, B., Thibodeau, D. & Setzer, A. (2013) Copatterns: Programming infinite structures by observations. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13, Rome, Italy, January 23-25, 2013, Giacobazzi, R. & Cousot, R. (eds). ACM, pp. 27-38. · Zbl 1301.68080
[8] Abel, A. & Scherer, G. (2012) On irrelevance and algorithmic equality in predicative type theory. Logical Methods Comput. Sci.8(1:29), 1-36. TYPES’10 special issue. · Zbl 1238.03028
[9] Abel, A. & Vezzosi, A. (2014) A formalized proof of strong normalization for guarded recursive types. In Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, Garrigue, J. (ed). Lecture Notes in Computer Science, vol. 8858. Springer, pp. 140-158. · Zbl 1453.68035
[10] Adams, R. (2006) Formalized metatheory with terms represented by an indexed family of types. In Types for Proofs and Programs,Filliâtre, J.-C., Paulin-Mohring, C. & Werner, B. (eds). Berlin, Heidelberg: Springer, pp. 1-16. · Zbl 1172.68547
[11] Ahmed, A. (2004) Semantics of Types for Mutable State. Ph.D. thesis, Princeton University.
[12] Ahmed, A. (2013) Logical relations. In Oregon Programming Languages Summer School (OPLSS).
[13] Ahmed, A., Fluet, M. & Morrisett, G. (2007) L^3: A linear language with locations. Fundam. Inform.77(4), 397-449. · Zbl 1121.68021
[14] Allais, G., Atkey, R., Chapman, J., Mcbride, C. & Mckinna, J. (2018). A type and scope safe universe of syntaxes with binding: Their semantics and proofs. Proc. ACM Program. Lang. 2(ICFP), 90:1-90:30. · Zbl 1522.68118
[15] Allais, G., Chapman, J., Mcbride, C. & Mckinna, J. (2017) Type-and-scope safe programs and their proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. CPP 2017. New York, NY, USA: ACM, pp. 195-207. · Zbl 1522.68118
[16] Altenkirch, T. (1992) Brewing Strong Normalization Proof with LEGO. Technical report 92-230. LFCS, Edinburgh. http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-230/ECS-LFCS-92-230.pdf.
[17] Altenkirch, T. (1993) A formalization of the strong normalization proof for System F in LEGO. In Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, Bezem, M. & Groote, J. F. (eds). Lecture Notes in Computer Science, vol. 664. Springer, pp. 13-28. · Zbl 0797.68095
[18] Altenkirch, T., Chapman, J. & Uustalu, T. (2014) Relative monads formalised. J. Formalized Reasoning7(1), 1-43. · Zbl 1451.68330
[19] Altenkirch, T., Chapman, J. & Uustalu, T. (2015) Monads need not be endofunctors. Log. Methods Comput. Sci.11(1). · Zbl 1448.18007
[20] Altenkirch, T., Hofmann, M. & Streicher, T. (1995) Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, 6th International Conference, CTCS’95, Cambridge, UK, August 7-11, 1995, Proceedings, Pitt, D. H., Rydeheard, D. E. & Johnstone, P. (eds). Lecture Notes in Computer Science, vol. 953. Springer, pp. 182-199. · Zbl 1502.03019
[21] Altenkirch, T. & Kaposi, A. (2016) Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Bodík, R. & Majumdar, R. (eds). ACM, pp. 18-29. · Zbl 1347.68045
[22] Altenkirch, T. & Kaposi, A. (2017) Normalisation by evaluation for type theory, in type theory. Logical Methods Comput. Sci.13(4:1), 1-26. · Zbl 1459.03013
[23] Altenkirch, T. & Mcbride, C. (2003) Generic programming within dependently typed programming. In Proceedings of the IFIP TC2/WG2.1 Working Conference on Generic Programming. Deventer, The Netherlands, The Netherlands: Kluwer, B.V., pp. 1-20. · Zbl 1089.68529
[24] Anand, A. (2016) Exploiting uniformity in substitution: The Nuprl term model. In The 5th International Congress on Mathematical Software (ICMS 2016).
[25] Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J., Pierce, B., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S. & Zdancewic, S. (2005) Mechanized metatheory for the masses: The POPLmark challenge. In Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Hurd, J. & Melham, T. F. (eds). Lecture Notes in Computer Science, vol. 3603. Springer, pp. 50-65. · Zbl 1152.68516
[26] Aydemir, B. & Weirich, S. (2010) LNgen: Tool Support for Locally Nameless Representations. Technical report. MS-CIS-10-24. University of Pennsylvania.
[27] Bengtson, J., Parrow, J. & Weber, T. (2016) Psi-calculi in isabelle. J. Autom. Reasoning56(1), 1-47. · Zbl 1356.68175
[28] Benke, M., Dybjer, P. & Jansson, P. (2003) Universes for generic programs and proofs in dependent type theory. Nordic J. Comput.10(4), 265-289. · Zbl 1094.68012
[29] Benton, N., Hur, C.-K., Kennedy, A. & Mcbride, C. (2012) Strongly typed term representations in Coq. J. Autom. Reasoning49(2), 141-159. · Zbl 1269.68041
[30] Berger, U., Berghofer, S., Letouzey, P. & Schwichtenberg, H. (2006) Program extraction from normalization proofs. Studia Logica82(1), 25-49. · Zbl 1095.03016
[31] Berghofer, S. (2004) Extracting a normalization algorithm in Isabelle/HOL. In TYPES. Lecture Notes inComputer Science, vol. 3839. Springer, pp. 50-65. · Zbl 1172.68613
[32] Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A. & Traytel, D. (2017) Friends with benefits. In Proceedings of the 26th European Symposium on Programming Languages and Systems - Volume 10201. New York, NY, USA: Springer-Verlag New York, Inc, pp. 111-140. · Zbl 1485.68280
[33] Cave, A. & Pientka, B. (2012) Programming with binders and indexed data-types. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, Field, J. & Hicks, M. (eds). ACM, pp. 413-424. · Zbl 1321.68141
[34] Cave, A. & Pientka, B. (2013) First-class substitutions in contextual type theory. In 8th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’13). ACM, pp. 15-24.
[35] Cave, A. & Pientka, B. (2015) A case study on logical relations using contextual types. In Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, August 1, 2015, Cervesato, I. & Chaudhuri, K. (eds). EPTCS, vol. 185.
[36] Cave, A. & Pientka, B. (2018) Mechanizing proofs with logical relations - Kripke-style. Math. Struct. Comput. Sci.28(9), 1606-1638. · Zbl 1400.68193
[37] Cervesato, I. & Pfenning, F. (2002) A linear logical framework. Inf. Comput.179(1), 19-75. cited By 52. · Zbl 1031.03056
[38] Chapman, J. (2009) Type theory should eat itself. Electr. Notes Theor. Comput. Sci. 228, 21-36. Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008). · Zbl 1337.68057
[39] Chapman, J., Dagand, P., Mcbride, C. & Morris, P. (2010) The gentle art of levitation. Sigplan Not.45(9), 3-14. · Zbl 1323.68239
[40] Charguéraud, A. (2012) The locally nameless representation. J. Autom. Reasoning49(3), 363-408. · Zbl 1260.68368
[41] Cheney, J. (2005) Toward a general theory of names: Binding and scope. In ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, Momigliano, A. & Pollack, R. (eds). ACM, pp. 33-40.
[42] Cheney, J. & Momigliano, A. (2017) α check: A mechanized metatheory model checker. TPLP17(3), 311-352. · Zbl 1379.68236
[43] Chlipala, A. (2008) Parametric higher-order abstract syntax for mechanized semantics. In ACM Sigplan Notices, vol. 43. ACM, pp. 143-156. · Zbl 1323.68184
[44] Coquand, C. (1993) From semantics to rules: A machine assisted analysis. In Computer Science Logic, 7th Workshop, CSL’93, Swansea, United Kingdom, September 13-17, 1993, Papers, Selected, Börger, E., Gurevich, Y. & Meinke, K. (eds), Lecture Notes in Computer Science, vol. 832. Springer, pp. 91-105. · Zbl 0953.68569
[45] Crary, K. (2005) Logical relations and a case study in equivalence checking. In Advanced Topics in Types and Programming Languages,Pierce, B. C. (ed). MIT.
[46] Curien, P.-L., Hardin, T. & Roís, A. (1992) Strong normalization of substitutions. In Mathematical Foundations of Computer Science 1992, 17th International Symposium, MFCS’92, Prague, Czechoslovakia, August 24-28, 1992, Proceedings, Havel, I. M., & Koubek, V. (eds). Lecture Notes in Computer Science, vol. 629. Springer, pp. 209-217. · Zbl 1496.03059
[47] Danielsson, N. A. (2007) A formalisation of a dependently typed language as an inductive-recursive family. In Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, Altenkirch, T. & Mcbride, C. (eds). Lecture Notes in Computer Science, vol. 4502. Springer, pp. 93-109. · Zbl 1178.03026
[48] De Bruijn, N. G. (1972) Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes Mathematicae (Proceedings), vol. 75. Elsevier, pp. 381-392. · Zbl 0253.68007
[49] Despeyroux, J., Felty, A. P. & Hirschowitz, A. (1995) Higher-order abstract syntax in coq. In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA’95, Edinburgh, UK, April 10-12, 1995, Proceedings, Dezani-Ciancaglini, M. & Plotkin, G. D. (eds). Lecture Notes in Computer Science, vol. 902. Springer, pp. 124-138. · Zbl 1063.68650
[50] Dybjer, P. (1994) Inductive families. Formal Aspects Comput6(4), 440-465. · Zbl 0808.03044
[51] Dybjer, P. & Setzer, A. (1999) A finite axiomatization of inductive-recursive definitions. In Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings, Girard, J.-Y. (ed). Lecture Notes in Computer Science, vol. 1581. Springer, pp. 129-146. · Zbl 0931.03069
[52] Felty, A. & Momigliano, A. (2012) Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reasoning48(1), 43-105. · Zbl 1252.68252
[53] Felty, A. P. & Momigliano, A. (2009) Reasoning with hypothetical judgments and open terms in Hybrid. In 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’09). New York, NY, USA: ACM, pp. 83-92.
[54] Felty, A. P., Momigliano, A. & Pientka, B. (2015) The next 700 challenge problems for reasoning with higher-order abstract syntax representations - part 2 - A survey. J. Autom. Reasoning55(4), 307-372. · Zbl 1357.68198
[55] Felty, A. P., Momigliano, A. & Pientka, B. (2018) Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci.28(9), 1507-1540. · Zbl 1400.68194
[56] Ferreira, F., Monnier, S. & Pientka, B. (2013) Compiling contextual objects: Bringing higher-order abstract syntax to programmers. In Proceedings of the 7th workshop on Programming languages meets program verification. ACM, pp. 13-24.
[57] Friedman, H. (1975) Equality between functionals. In Logic Colloquium,Parikh, R. (ed). Lecture Notes in Mathematics, vol. 453. Springer, pp. 22-37. · Zbl 0311.02040
[58] Gacek, A. (2010) Girard’s Proof of Strong Normalization of the Simply-Typed Lambda-Calculus Calculus. http://abella-prover.org/examples/lambda-calculus/normalization/stlc-strong-norm.html.
[59] Geuvers, H. (1995) A short and flexible proof of strong normalization for the calculus of constructions. In Selected Papers from the International Workshop on Types for Proofs and Programs. TYPES’94. London, UK: Springer-Verlag, pp. 14-38.
[60] Girard, J. Y. (1972) Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur. These d’état, Université de Paris 7.
[61] Girard, J.-Y., Lafont, Y. & Taylor, P. (1989) Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University. · Zbl 0671.68002
[62] Goguen, H. (1995) Typed operational semantics. In 2nd International Conference on Typed Lambda Calculi and Applications (TLCA’95), Dezani-Ciancaglini, M. & Plotkin, G. (eds). Lecture Notes in Computer Science (LNCS 902). Springer, pp. 186-200. · Zbl 1063.68556
[63] Goguen, H. (2005) Justifying algorithms for βη conversion. In Foundations of Software Science and Computational Structures, 8th International Conference, FoSSaCS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, Sassone, V. (ed). Lecture Notes in Computer Science, vol. 3441. Springer, pp. 410-424. · Zbl 1119.03024
[64] Group, Nominal Methods (2009) Strong normalization for the simply typed lambda calculus. https://isabelle.in.tum.de/dist/library/HOL/HOL-Nominal-Examples/SN.html.
[65] Harper, R., Honsell, F. & Plotkin, G. D. (1993) A framework for defining logics. J. Associat. Comput. Mach.40(1), 143-184. · Zbl 0778.03004
[66] Harper, R. & Pfenning, F. (2005) On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Logic6(1), 61-101. · Zbl 1367.03055
[67] Hoare, T. (2003) The verifying compiler: A grand challenge for computing research. In Modular Programming Languages,Böszörményi, L. & Schojer, P. (eds). Berlin, Heidelberg: Springer, pp. 25-35. · Zbl 1032.68868
[68] Hofmann, M. (1999) Semantical analysis of higher-order abstract syntax. In 14th Symposium on Logic in Computer Science, 1999. Proceedings. IEEE, pp. 204-213.
[69] Hur, C.-K., Neis, G., Dreyer, D. & Vafeiadis, V. (2013) The power of parameterization in coinductive proof. In POPL’13. NY, USA: ACM, pp. 193-206. · Zbl 1301.68220
[70] Jacob-Rao, R., Pientka, B. & Thibodeau, D. (2018) Index-stratified types. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, Uk, Kirchner, H. (ed). LIPIcs, vol. 108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 19:1-19:17. · Zbl 1462.68021
[71] Joachimski, F. & Matthes, R. (2003) Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Arch. Math. Logic42(1), 59-87. · Zbl 1025.03010
[72] Kaiser, J., Schäfer, S. & Stark, K. (2017) Autosubst 2: Towards reasoning with multi-sorted de Bruijn terms and vector substitutions. In Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. LFMTP’17. New York, NY, USA: ACM, pp. 10-14.
[73] Keuchel, S., Weirich, S. & Schrijvers, T. (2016) Needle & Knot: Binder boilerplate tied up. In European Symposium on Programming. Springer, pp. 419-445.
[74] Klein, G. & Nipkow, T. (2006) A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst.28(4), 619-695.
[75] Kumar, R., Myreen, M. O., Norrish, M. & Owens, S. (2014) CakeML: A verified implementation of ML. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14, San Diego, CA, USA, January 20-21, 2014, Jagannathan, S. & Sewell, P. (eds). ACM, pp. 179-192. · Zbl 1284.68405
[76] Lee, D. K., Crary, K. & Harper, R. (2007) Towards a mechanized metatheory of standard ML. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, Hofmann, M. & Felleisen, M. (eds). ACM, pp. 173-184. · Zbl 1295.68088
[77] Lee, G., Oliveira, B. C. D. S., Cho, S. & Yi, K. (2012) GMeta: A generic formal metatheory framework for first-order representations. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24-April 1, 2012. Proceedings, Seidl, H. (ed). Lecture Notes in Computer Science, vol. 7211. Springer, pp. 436-455. · Zbl 1352.68063
[78] Lenglet, S. & Schmitt, A. (2018) Hoπ in Coq. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2018. New York, NY, USA: ACM, pp. 252-265.
[79] Leroy, X. (2009) Formal verification of a realistic compiler. Commun. ACM52(7), 107-115.
[80] Licata, D. R. & Harper, R. (2009) A universe of binding and computation. In ACM Sigplan Notices, vol. 44. ACM, pp. 123-134. · Zbl 1302.68050
[81] Mahmoud, M. Y. & Felty, A. P. (2019) Formalization of metatheory of the quipper quantum programming language in a linear logic. J. Autom. Reasoning63(4), 967-1002. · Zbl 1468.68330
[82] Malcolm, G. (1990) Data structures and program transformation. Sci. Comput. Program.14(2-3), 255-279. · Zbl 0712.68014
[83] Martin-Löf, P. (1982) Constructive mathematics and computer programming. Stud. Logic Foundat. Math.104, 153-175. · Zbl 0541.03034
[84] Mitchell, J. C. & Moggi, E. (1991) Kripke-style models for typed lambda calculus. Ann. Pure Appl. Logic51(1-2), 99-124. · Zbl 0728.03011
[85] Momigliano, A. (2012) A supposedly fun thing I may have to do again: A HOAS encoding of Howe’s method. In Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-languages, Theory and Practice. LFMTP’12. New York, NY, USA: ACM, pp. 33-42.
[86] Momigliano, A., Pientka, B. & Thibodeau, D. (2019) A case study in programming coinductive proofs: Howe’s method. Math. Struct. Comput. Sci.29(8), 1309-1343. · Zbl 1430.68418
[87] Nanevski, A., Pfenning, F. & Pientka, B. (2008) Contextual modal type theory. ACM Trans. Comput. Logic9(3), 1-49. · Zbl 1367.03060
[88] Narboux, J. & Urban, C. (2008) Formalising in Nominal Isabelle Crary’s completeness proof for equivalence checking. Electronic Notes Theoret. Comput. Sci. 196, 3-18. Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007). · Zbl 1278.68276
[89] Norell, U. (2009) Dependently typed programming in Agda. In AFP Summer School.Springer, pp. 230-266. · Zbl 1263.68038
[90] Pérez, J. A., Caires, L., Pfenning, F. & Toninho, B. (2014) Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput.239, 254-302. · Zbl 1309.68141
[91] Pickering, M., Érdi, G., Peyton Jones, S. & Eisenberg, R. A. (2016) Pattern synonyms. In Proceedings of the 9th International Symposium on Haskell. Haskell 2016. New York, NY, USA: ACM, pp. 80-91.
[92] Pientka, B. (2005) Verifying termination and reduction properties about higher-order logic programs. J. Autom. Reasoning34(2), 179-207. · Zbl 1102.68648
[93] Pientka, B. (2007) Proof pearl: The power of higher-order encodings in the logical framework LF. In Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, Schneider, K. & Brandt, J. (eds). Lecture Notes in Computer Science, vol. 4732. Springer, pp. 246-261. · Zbl 1144.68365
[94] Pientka, B. (2008) A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, Necula, G. C. & Wadler, P. (eds). ACM, pp. 371-382. · Zbl 1295.68068
[95] Pientka, B. & Dunfield, J. (2010) Beluga: A framework for programming and reasoning with deductive systems (system description). In 5th International Joint Conference on Automated Reasoning (IJCAR’10), Giesl, J. & Haehnle, R. (eds). Lecture Notes in Artificial Intelligence (LNAI 6173). Springer, pp. 15-21. · Zbl 1291.68366
[96] Pierce, B. C. (2002) Types and Programming Languages. MIT. · Zbl 0995.68018
[97] Pierce, B. C. & Weirich, S. (2012) Introduction to the special issue on the POPLMark Challenge. J. Autom. Reasoning49(3), 301-302.
[98] Plotkin, G. (1973) Lambda-Definability and Logical Relations. Memorandum sai-rm-4. University of Edinburgh.
[99] Pollack, R. (1994) Closure under alpha-conversion. In Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Papers, Selected, Barendregt, H. & Nipkow, T. (eds). Lecture Notes in Computer Science, vol. 806. Springer, pp. 313-332.
[100] Pouillard, N. & Pottier, F. (2010) A fresh look at programming with names and binders. In ACM Sigplan Notices, vol. 45. ACM, pp. 217-228. · Zbl 1323.68082
[101] Poulsen, C. B., Rouvoet, A., Tolmach, A., Krebbers, R. & Visser, E. (2018). Intrinsically-typed definitional interpreters for imperative languages. PACMPL2(POPL), 16:1-16:34.
[102] Rasmussen, U. & Filinski, A. (2013) Structural logical relations with case analysis and equality reasoning. In Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, Momigliano, A., Pientka, B. & Pollack, R. (eds). ACM, pp. 43-54.
[103] Rizkallah, C., Garbuzov, D. & Zdancewic, S. (2018) A formal equational theory for call-by-push-value. In International Conference on Interactive Theorem Proving. Springer, pp. 523-541. · Zbl 1511.68086
[104] Rossberg, A., Russo, C. & Dreyer, D. (2014) F-ing modules. J. Funct. Program.24(5), 529-607. · Zbl 1322.68048
[105] Schäfer, S., Tebbi, T. & Smolka, G. (2014) Autosubst: Automation for de Bruijn substitutions. In 6th Coq Workshop, July 2014. · Zbl 1465.68037
[106] Schäfer, S., Smolka, G. & Tebbi, T. (2015) Completeness and decidability of de Bruijn substitution algebra in Coq. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. Berlin, Heidelberg: Springer-Verlag, pp. 67-73.
[107] Schürmann, C. & Sarnat, J. (2008) Structural logical relations. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, June 24-27, 2008, Pittsburgh, Pa, Usa, Pfenning, F. (ed). IEEE Computer Society, pp. 69-80.
[108] Sturm, S. (2018) Verification and Theorem Proving in F*. M.Phil. thesis, LMU. https://github.com/sturmsebastian/Fstar-master-thesis-code.
[109] Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Logic32(2), 198-212. · Zbl 0174.01202
[110] Tiu, A. & Miller, D. (2010) Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log. 11(2), 13:1-13:35. · Zbl 1351.68186
[111] Urban, C. & Kaliszyk, C. (2012) General bindings and alpha-equivalence in nominal isabelle. Log. Methods Comput. Sci.8(2:14), 1-35. · Zbl 1242.68283
[112] Urban, C., Cheney, J. & Berghofer, S. (2011) Mechanizing the metatheory of LF. ACM Trans. Comput. Logic12(2), 15:1-15:42. · Zbl 1351.68250
[113] Van Raamsdonk, F. & Severi, P. (1995) On Normalisation. Technical report 95/20. Technische Universiteit Eindhoven.
[114] Wang, Y., Chaudhuri, K., Gacek, A. & Nadathur, G. (2013) Reasoning about higher-order relational specifications. In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming. ACM, pp. 157-168.
[115] Watkins, K., Cervesato, I., Pfenning, F. & Walker, D. (2002) A Concurrent Logical Framework I: Judgments and Properties. Technical report CMU-CS-02-101. Department of Computer Science, Carnegie Mellon University. · Zbl 1100.68548
[116] Weirich, S., Yorgey, B. A. & Sheard, T. (2011) Binders unbound. In ACM SIGPLAN Notices, vol. 46. ACM, pp. 333-345. · Zbl 1323.68177
[117] Werner, B. (1992) A normalization proof for an impredicative type system with large elimination over integers. In International Workshop on Types for Proofs and Programs (TYPES), pp. 341-357.
[118] Xi, H. (2004) Applied type system. In TYPES 2003. Lecture Notes in Computer Science, vol. 3085. Springer, pp. 394-408. · Zbl 1100.03518
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.