Abstract
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term-constructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our extension includes new definitions of α-equivalence and establishes automatically the reasoning infrastructure for α-equated terms. We also prove strong induction principles that have the usual variable convention already built in.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N.: PiSigma: Dependent Types Without the Sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 40–55. Springer, Heidelberg (2010)
Bengtson, J., Parrow, J.: Psi-Calculi in Isabelle. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 99–114. Springer, Heidelberg (2009)
Charguéraud, A.: The Locally Nameless Representation. To appear in J. of Automated Reasoning
Cheney, J.: Scrap your Nameplate (Functional Pearl). In: Proc. of the 10th ICFP Conference, pp. 180–191 (2005)
Cheney, J.: Toward a General Theory of Names: Binding and Scope. In: Proc. of the 3rd MERLIN Workshop, pp. 33–40 (2005)
Homeier, P.: A Design Structure for Higher Order Quotients. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 130–146. Springer, Heidelberg (2005)
Huffman, B., Urban, C.: Proof Pearl: A New Foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 35–50. Springer, Heidelberg (2010)
Kaliszyk, C., Urban, C.: Quotients Revisited for Isabelle/HOL. To appear in the Proc. of the 26th ACM Symposium on Applied Computing (2011)
Lee, D.K., Crary, K., Harper, R.: Towards a Mechanized Metatheory of Standard ML. In: Proc. of the 34th POPL Symposium, pp. 173–184 (2007)
Naraschewski, W., Nipkow, T.: Type Inference Verified: Algorithm W in Isabelle/HOL. J. of Automated Reasoning 23, 299–318 (1999)
Pitts, A.: Notes on the Restriction Monad for Nominal Sets and Cpos. Unpublished notes for an invited talk given at CTCS (2004)
Pitts, A.M.: Nominal Logic, A First Order Theory of Names and Binding. Information and Computation 183, 165–193 (2003)
Pottier, F.: An Overview of Cαml. In: ACM Workshop on ML. ENTCS, vol. 148, pp. 27–52 (2006)
Sato, M., Pollack, R.: External and Internal Syntax of the Lambda-Calculus. J. of Symbolic Computation 45, 598–616 (2010)
Sewell, P.: A Binding Bestiary. Unpublished notes
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: OTT: Effective Tool Support for the Working Semanticist. J. of Functional Programming 20(1), 70–122 (2010)
Tobin-Hochstadt, S., Felleisen, M.: The Design and Implementation of Typed Scheme. In: Proc. of the 35rd POPL Symposium, pp. 395–406 (2008)
Urban, C., Cheney, J., Berghofer, S.: Mechanizing the Metatheory of LF. In: Proc. of the 23rd LICS Symposium, pp. 45–56 (2008)
Urban, C., Nipkow, T.: Nominal Verification of Algorithm W. In: Huet, G., Lévy, J.-J., Plotkin, G. (eds.) From Semantics to Computer Science. Essays in Honour of Gilles Kahn, pp. 363–382. Cambridge University Press, Cambridge (2009)
Urban, C., Tasson, C.: Nominal techniques in isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005)
Urban, C., Zhu, B.: Revisiting Cut-Elimination: One Difficult Proof is Really a Proof. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 409–424. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urban, C., Kaliszyk, C. (2011). General Bindings and Alpha-Equivalence in Nominal Isabelle. In: Barthe, G. (eds) Programming Languages and Systems. ESOP 2011. Lecture Notes in Computer Science, vol 6602. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19718-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-19718-5_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19717-8
Online ISBN: 978-3-642-19718-5
eBook Packages: Computer ScienceComputer Science (R0)