Advertisement

Journal of Automated Reasoning

, Volume 40, Issue 4, pp 327–356 | Cite as

Nominal Techniques in Isabelle/HOL

  • Christian Urban
Article

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.

Keywords

Lambda-calculus Nominal logic work Theorem provers 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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 2002Google Scholar
  2. 2.
    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 2006Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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 2005Google Scholar
  5. 5.
    Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1981)Google Scholar
  6. 6.
    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 2007Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. Inf. Comput. 157, 183–235 (2000)MATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gabbay, M.J.: A theory of inductive definitions with α-equivalence. PhD thesis, University of Cambridge (2001)Google Scholar
  11. 11.
    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341–363 (2001)CrossRefGoogle Scholar
  12. 12.
    Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)Google Scholar
  13. 13.
    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 1994Google Scholar
  14. 14.
    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 1996Google Scholar
  15. 15.
    Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1), 61–101 (2005)CrossRefMathSciNetGoogle Scholar
  16. 16.
    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 2005Google Scholar
  17. 17.
    Kleene, S.C.: Disjunction and existence under implication in elementary intuitionistic formalisms. J. Symb. Log. 27(1), 11–18 (1962)CrossRefMathSciNetGoogle Scholar
  18. 18.
    Leroy, X.: Polymorphic typing of an algorithmic language. Ph.D. thesis, University Paris 7, INRIA Research Report, No 1778 (1992)Google Scholar
  19. 19.
    Melham, T.: Automating recursive type definitions in higher order logic. Technical Report 146, Computer Laboratory, University of Cambridge, September (1988)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: A proof assistant for higher-order logic. LNCS, vol. 2283. Springer, New York (2002)Google Scholar
  22. 22.
    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 2004Google Scholar
  23. 23.
    Norrish, M.: Mechanising λ-calculus using a classical first order theory of terms with permutation. High. Order Symb. Comput. 19, 169–195 (2006)MATHCrossRefGoogle Scholar
  24. 24.
    Paulson, L.: Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4), 658–675 (2006)MathSciNetCrossRefGoogle Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 165–193 (2003)MATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53, 459–506 (2006)CrossRefMathSciNetGoogle Scholar
  28. 28.
    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 2000Google Scholar
  29. 29.
    Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995)MATHCrossRefGoogle Scholar
  30. 30.
    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)Google Scholar
  31. 31.
    Urban, C.: Classical logic and computation. Ph.D. thesis, Cambridge University, October (2000)Google Scholar
  32. 32.
    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 2006Google Scholar
  33. 33.
    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 2007Google Scholar
  34. 34.
    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)CrossRefGoogle Scholar
  35. 35.
    Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comp. Sci. 323(1–2), 473–497 (2004)MATHCrossRefMathSciNetGoogle Scholar
  36. 36.
    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 2005Google Scholar
  37. 37.
    Wenzel, M.: Using axiomatic type classes in Isabelle. Manual in the Isabelle distribution. http://isabelle.in.tum.de/doc/axclass.pdf (2000)
  38. 38.
    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 2006Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2008

Authors and Affiliations

  1. 1.Technical University MunichMunichGermany

Personalised recommendations