Abstract
This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that is bijective with the alpha-equated lambda-terms. Unlike de-Bruijn indices, however, this inductive set includes names and reasoning about it is very similar to informal reasoning with “pencil and paper”. To show this we provide a structural induction principle that requires to prove the lambda-case for fresh binders only. Furthermore, we adapt work by Pitts providing a recursion combinator for the inductive set. The main technical novelty of this work is that it is compatible with the axiom of choice (unlike earlier nominal logic work by Pitts et al); thus we were able to implement all results in Isabelle/HOL and use them to formalise the standard proofs for Church-Rosser, strong-normalisation of beta-reduction, the correctness of the type-inference algorithm W, typical proofs from SOS and much more.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ambler, S.J., Crole, R.L., Momigliano, A.: Combining higher order abstract syntax with tactical theorem proving and (co)induction. In: Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 2410, pp. 13–30. Hampton, 20–23 August 2002
Aydemir, B., Bohannon, A., Weihrich, S.: Nominal reasoning techniques in Coq (work in progress). In: Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP). ENTCS, pp. 60–68. Seattle, 16 August 2006
Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35rd Symposium on Principles of Programming Languages (POPL), pp. 3–15. ACM, New York (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: Proceedings of the 18th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs). LNCS, vol. 3603, pp. 50–65. Oxford, 22–25 August 2005
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1981)
Bengtson, J., Parrow, J.: Formalising the pi-Calculus using nominal logic. In: Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS). LNCS, vol. 4423, pp. 63–77. Braga, March 2007
Crary, K.: Logical relations and a case study in equivalence checking. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 223–244. MIT, Cambridge (2005)
Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications (TLCA). LNCS, vol. 902, pp. 124–138. Springer, New York (1995)
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. Inf. Comput. 157, 183–235 (2000)
Gabbay, M.J.: A theory of inductive definitions with α-equivalence. PhD thesis, University of Cambridge (2001)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341–363 (2001)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)
Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Proceedings of the 6th International Workshop on Higher-order Logic Theorem Proving and its Applications (HUG). LNCS, vol. 780, pp. 414–426. Vancouver, 11–13 August 1994
Gordon, A.D., Melham, T.: Five axioms of alpha conversion. In: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 1125, pp. 173–190. Turku, 26–30 August 1996
Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1), 61–101 (2005)
Homeier, P.: A design structure for higher order quotients. In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 3603, pp. 130–146. Oxford, 22–25 August 2005
Kleene, S.C.: Disjunction and existence under implication in elementary intuitionistic formalisms. J. Symb. Log. 27(1), 11–18 (1962)
Leroy, X.: Polymorphic typing of an algorithmic language. Ph.D. thesis, University Paris 7, INRIA Research Report, No 1778 (1992)
Melham, T.: Automating recursive type definitions in higher order logic. Technical Report 146, Computer Laboratory, University of Cambridge, September (1988)
Melham, T.: Automating recursive type definitions in higher order logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 341–386. Springer, New York (1989)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: A proof assistant for higher-order logic. LNCS, vol. 2283. Springer, New York (2002)
Norrish, M.: Recursive function definition for types with binders. In: Proceedings of the 17th International Conference Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 3223, pp. 241–256. Park City, 14–17 September 2004
Norrish, M.: Mechanising λ-calculus using a classical first order theory of terms with permutation. High. Order Symb. Comput. 19, 169–195 (2006)
Paulson, L.: Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4), 658–675 (2006)
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the 10th Conference on Conference on Programming Language Design and Implementation (PLDI), pp. 199–208. ACM, New York (1989)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 165–193 (2003)
Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53, 459–506 (2006)
Slind, K.: Wellfounded schematic definitions. In: Proceedings of the 17th International Conference on Automated Deduction (CADE). LNCS, vol. 1831, pp. 45–63. Pittsburgh, 17–20 June 2000
Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995)
Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: Proceedings of the 35rd Symposium on Principles of Programming Languages (POPL), pp. 395–406. ACM, New York (2008)
Urban, C.: Classical logic and computation. Ph.D. thesis, Cambridge University, October (2000)
Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle/HOL. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR). LNAI, vol. 4130, pp. 498–512. Seattle, 17–20 August 2006
Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: Proceedings of the 21st International Conference on Automated Deduction (CADE). LNAI, vol. 4603, pp. 35–50. Bremen, 17–20 July 2007
Urban, C., Norrish, M.: A formal treatment of the Barendregt variable convention in rule inductions. In: Proceedings of the 3rd International ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names, pp. 25–32. ACM, New York (2005)
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comp. Sci. 323(1–2), 473–497 (2004)
Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Proceedings of the 20th International Conference on Automated Deduction (CADE). LNCS, vol. 3632, pp. 38–53. Tallinn, 22–27 July 2005
Wenzel, M.: Using axiomatic type classes in Isabelle. Manual in the Isabelle distribution. http://isabelle.in.tum.de/doc/axclass.pdf (2000)
Wenzel, M.: Structured induction proofs in Isabelle/Isar. In: Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM). LNAI, vol. 4108, pp. 17–30. Wokingham, 11–12 August 2006
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Urban, C. Nominal Techniques in Isabelle/HOL. J Autom Reasoning 40, 327–356 (2008). https://doi.org/10.1007/s10817-008-9097-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-008-9097-2