Abstract
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?
We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F< :, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Appel, A.W.: Foundational proof-carrying code. In: IEEE Symposium on Logic in Computer Science (LICS), Boston, Massachusetts, June 2001, pp. 247–258 (2001)
Cardelli, L.: Extensible records in a pure calculus of subtyping. Research report 81, DEC/Compaq Systems Research Center (January 1992) Also In: Gunter, C.A., Mitchell, J.C. (eds.) Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, Cambridge (1994)
Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of System F with subtyping. Information and Computation 109(1–2), 4–56 (1994); Summary in TACS 1991 (Sendai, Japan, pp. 750–770) (1991)
Crary, K.: Toward a foundational typed assembly language. In: ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana, January 2003, pp. 198–212 (2003)
Dennis, L.A.: Inductive challenge problems (2000), http://www.cs.nott.ac.uk/~lad/research/challenges
Dubois, C., Menissier-Morain, V.: Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning 23(3-4), 319–346 (1999)
Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol. 19, pp. 19–32. American Mathematical Society, Providence (1967)
Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: 14th Symposium on Logic in Computer Science, pp. 214–224 (1999)
Gent, I.P., Walsh, T.: CSPLib: a benchmark library for constraints. Technical Report APES-09-1999, APES. A shorter version appears in the Proceedings of the 5th International Conference on Principles and Practices of Constraint Programming, CP-99 (1999), Available from http://www.dcs.st-and.ac.uk/~apes/apesreports.html
Ghelli, G.: Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Università di Pisa, Technical report TD–6/90, Dipartimento di Informatica, Università di Pisa (1990)
Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 173–190. Springer, Heidelberg (1996)
Green, I.: The dream corpus of inductive conjectures (1999), http://dream.dai.ed.ac.uk/dc/lib.html
Gunter, E., Maharaj, S.: Studying the ML module system in HOL. The Computer Journal: Special Issue on Theorem Proving in Higher Order Logics 38(2), 142–151 (1995)
Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003)
Hoos, H., Stuetzle, T.: SATLIB., http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/
Joyce, J.J., Seger, C.-J.H. (eds.): HUG 1993. LNCS, vol. 780. Springer, Heidelberg (1994)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, Sydney (March 2004)
McKinna, J., Pollack, R.: James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3–4) (November 1999)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML, Revised edition. MIT Press, Cambridge (1997)
Moore, J.S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)
Moore, J.S., Porter, G.: The apprentice challenge. ACM Trans. Program. Lang. Syst. 24(3), 193–216 (2002)
Naraschewski, W., Nipkow, T.: Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23, 299–318 (1999)
Nipkow, T., von Oheimb, D., Pusch, C.: μJava: Embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbrüggen, R. (eds.) Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pp. 117–144. IOS Press, Amsterdam (2000)
Nipkow, T., von Oheimb, D.: Javalight is type-safe—definitely. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161–170. ACM Press, New York (1998)
Norrish, M.: Formalising C in HOL. PhD thesis, Computer Laboratory, University of Cambridge (1998)
Norrish, M.: Mechanising Hankin and Barendregt using the Gordon-Melham axioms. In: MERLIN 2003: Proceedings Of The 2003 Workshop On Mechanized Reasoning About Languages With Variable Binding, pp. 1–7. ACM Press, New York (2003)
Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 241–256. Springer, Heidelberg (2004)
Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI 1988: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, pp. 199–208. ACM Press, New York (1988)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)
Sutcliffe, G., Suttner, C.: The TPTP problem library. Journal of Automated Reasoning 21(2), 177–203 (1998)
Syme, D.: Reasoning with the formal definition of Standard ML in HOL. In: Joyce and Seger [16], pp. 43–60
Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. Accepted at CADE-20 in Tallinn. See http://www.mathematik.uni-muenchen.de/~urban/nominal/
VanInwegen, M., Gunter, E.: HOL-ML. In: Joyce and Seger [16], pp. 61–74
Vestergaard, R., Brotherston, J.: The mechanisation of Barendregt-style equational proofs (the residual perspective). In: Mechanized Reasoning about Languages with Variable Binding (MERLIN). Electronic Notes in Theoretical Computer Science, vol. 58. Elsevier, Amsterdam (2001)
Vestergaard, R., Brotherston, J.: A formalised first-order confluence proof for the λ-calculus using one-sorted variable names. RTA 2001 183(2), 212–244 (2003); Special edition with selected papers from RTA 2001
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aydemir, B.E. et al. (2005). Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_4
Download citation
DOI: https://doi.org/10.1007/11541868_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)