Abstract
A long line of research has been dealing with the representation, in a formal tool such as an interactive theorem prover, of languages with binding structures (e.g. the lambda calculus). Several concrete encodings of binding have been proposed, including de Bruijn dummies, the locally nameless representation, and others. Each of these encodings has its strong and weak points, with no clear winner emerging. One common drawback to such techniques is that reasoning on them discloses too much information about what we could call “implementation details”: often, in a formal proof, an unbound index will appear out of nowhere, only to be substituted immediately after; such details are never seen in an informal proof. To hide this unnecessary complexity, we propose to represent binding structures by means of an abstract data type, equipped with high level operations allowing to manipulate terms with binding with a degree of abstraction comparable to that of informal proofs. We also prove that our abstract representation is sound by providing a de Bruijn model.
Chapter PDF
References
Adams, R.: A Modular Hierarchy of Logical Frameworks. Ph.D. thesis, University of Manchester (2004)
Ahrens, B., Zsido, J.: Initial semantics for higher-order typed syntax in Coq. Journal of Formalized Reasoning 4(1) (2011), http://jfr.unibo.it/article/view/2066
Asperti, A., et al.: Formal metatheory of programming languages in the Matita interactive theorem prover. Journal of Automated Reasoning: Special Issue on the Poplmark Challenge 49(3), 427–451 (2012)
Aydemir, B., Weirich, S.: LNgen: Tool support for locally nameless representations. Tech. Rep. MS-CIS-10-24, University of Pennsylvania, Department of Computer and Information Science (2010)
Aydemir, B.E., et al.: Mechanized metatheory for the masses: The poplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Berghofer, S., Urban, C.: Nominal inversion principles. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 71–85. Springer, Heidelberg (2008), http://dx.doi.org/10.1007/978-3-540-71067-7_10
Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. Journal of Functional Programming (1999)
Capretta, V., Felty, A.: Higher-order abstract syntax in type theory. In: Cooper, S.B., Geuvers, H., Pillay, A., Väänänen, J. (eds.) Logic Colloquium 2006. Lecture Notes in Logic, vol. 32, pp. 65–90. Cambridge University Press (2009)
Charguraud, A.: The locally nameless representation. Journal of Automated Reasoning 49(3), 363–408 (2012), http://dx.doi.org/10.1007/s10817-011-9225-2
Ciaffaglione, A., Scagnetto, I.: A weak HOAS approach to the POPLmark challenge. In: Kesner, D., Viana, P. (eds.) Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, Rio de Janeiro, Brazil, September 29-30. Electronic Proceedings in Theoretical Computer Science, vol. 113, pp. 109–124. Open Publishing Association (2013)
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), http://dx.doi.org/10.1007/BFb0105404
Huffman, B., Urban, C.: A new foundation for nominal isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 35–50. Springer, Heidelberg (2010), http://dx.doi.org/10.1007/978-3-642-14052-5_5
McBride, C.: Dependently Typed Functional Programs and their Proofs. Ph.D. thesis, University of Edinburgh (1999)
McBride, C.: Elimination with a motive. In: Callaghan, P., et al. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197–216. Springer, Heidelberg (2002)
McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3), 373–409 (1999), http://dx.doi.org/10.1023/A
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 381–392 (1972)
Pollack, R., Sato, M., Ricciotti, W.: A canonical locally named representation of binding. Journal of Automated Reasoning 49(2), 185–207 (2012), http://dx.doi.org/10.1007/s10817-011-9229-y
Polonowski, E.: Automatically generated infrastructure for de bruijn syntaxes. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 402–417. Springer, Heidelberg (2013), http://dx.doi.org/10.1007/978-3-642-39634-2_29
Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. pp. 346–358. ICFP 2011 ACM, New York (2011), http://doi.acm.org/10.1145/2034773.2034819
Pottier, F.: An overview of Cαml. Electronic Notes in Theoretical Computer Science 148(2), 27–52 (2006), Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005) ACM-SIGPLAN Workshop on ML 2005 (2005)
Pouillard, N.: Nameless, painless. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 320–332. ACM, New York (2011), http://doi.acm.org/10.1145/2034773.2034817
Ricciotti, W.: Theoretical and Implementation Aspects in the Mechanization of the Metatheory of Programming Languages. Ph.D. thesis, Università di Bologna (2011)
Sato, M., Pollack, R.: External and internal syntax of the lambda-calculus. J. Symb. Comput. 45(5), 598–616 (2010), http://dx.doi.org/10.1016/j.jsc.2010.01.010
Schäfer, S., Tebbi, T.: Autosubst: Automation for de Bruijn substitutions. In: 6th Coq Workshop (July 2014)
Urban, C.: Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning 40(4), 327–356 (2008), http://dx.doi.org/10.1007/s10817-008-9097-2
Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 480–500. Springer, Heidelberg (2011), http://dx.doi.org/10.1007/978-3-642-19718-5_25
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ricciotti, W. (2015). Binding Structures as an Abstract Data Type. In: Vitek, J. (eds) Programming Languages and Systems. ESOP 2015. Lecture Notes in Computer Science(), vol 9032. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46668-1
Online ISBN: 978-3-662-46669-8
eBook Packages: Computer ScienceComputer Science (R0)