Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-22T06:37:17.588Z Has data issue: false hasContentIssue false
  • English
  • Français

Romeo: A system for more flexible binding-safe programming*

Part of: JFP Research Articles

Published online by Cambridge University Press:  22 July 2016

PAUL STANSIFER  and
MITCHELL WAND
PAUL STANSIFER
Affiliation:
College of Computer and Information Science, Northeastern University Boston, Massachusetts, USA e-mail: [email protected] and [email protected]
MITCHELL WAND
Affiliation:
College of Computer and Information Science, Northeastern University Boston, Massachusetts, USA e-mail: [email protected] and [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Current systems for safely manipulating values containing names only support simple binding structures for those names. As a result, few tools exist to safely manipulate code in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects α-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's λm, but is a full-fledged binding-safe language like Pure FreshML.

Type
Articles
Information
Journal of Functional Programming , Volume 26 , 2016 , e13
Copyright
Copyright © Cambridge University Press 2016 

Footnotes

*

This material is based on research sponsored by the Defense Advanced Research Projects Agency and the Air Force Research Laboratory under agreement number FA8750-10-2-0233. Any opinions, findings, conclusions or recommendations expressed herein are those of the authors, and do not necessarily reflect those of the US Government, DARPA, or the Air Force.

References

Adams, M. D. (2015) Towards the essence of hygiene. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 457–469.Google Scholar
Aydemir, B. E., Bohannon, A., Fairbairn, M., Foster, J. N., Pierce, B. C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S. & Zdancewic, S. (2005). Mechanized metatheory for the masses: The PoplMark challenge. In Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics. Berlin, Heidelberg: Springer-Verlag, pp. 50–65.CrossRefGoogle Scholar
Clinger, W. & Rees, J. (1991). Macros that work. In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 155–162.Google Scholar
de Moura, L. & Bjørner, N. (2008). Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Berlin Heidelberg: Springer.Google Scholar
Dybvig, R. K., Hieb, R. & Bruggeman, C. (1992). Syntactic abstraction in scheme. LISP Symb. Comput. 5 (4), 295–326.Google Scholar
Erdweg, S., van der Storm, T. & Dai, Y. (2014). Capture-avoiding and hygienic program transformations. In ECOOP 2014 Object-Oriented Programming, Jones, R. (ed), Lecture Notes in Computer Science, vol. 8586, pp. 489–514. Berlin Heidelberg: Springer.Google Scholar
Flatt, M. (2016). Binding as sets of scopes. SIGPLAN Not. 51 (1), 705–717.Google Scholar
Hendriks, D. & van Oostrom, V. (2003). Adbmal. In Automated Deduction CADE-19, Baader, F. (ed), Lecture Notes in Computer Science, vol. 2741. Berlin Heidelberg: Springer, pp. 136–150.Google Scholar
Herman, D. (2010). A Theory of Typed Hygienic Macros. PhD Thesis, Boston, MA, USA: Northeastern University.Google Scholar
Herman, D. & Wand, M. (2008). A theory of hygienic macros. In Proceedings of the Theory and Practice of Software, 17th European Conference on Programming Languages and Systems. Berlin, Heidelberg: Springer-Verlag, pp. 48–62.Google Scholar
Kohlbecker, E., Friedman, D. P., Felleisen, M. & Duba, B. (1986). Hygienic macro expansion. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, LFP '86. New York, NY, USA: ACM, pp. 151–161.Google Scholar
Lorenzen, F. & Erdweg, S. (2016). Sound type-dependent syntactic language extension. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. New York, NY, USA: ACM.Google Scholar
Muehlboeck, F. (2013). Checking Binding Hygiene Statically. Master's Thesis, Boston, MA, USA: Northeastern University.Google Scholar
Pollack, R., Sato, M. & Ricciotti, W. (2012). A canonical locally named representation of binding. J. Autom. Reason. 49 (2), 185–207.CrossRefGoogle Scholar
Pottier, F. (2006). An overview of Cαml. Electron. Notes Theor. Comput. Sci. 148 (2), 27–52.Google Scholar
Pottier, F. (2007a). Static Name Control for FreshML. Available at: http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml-long.pdf. [4 July, 2016]Google Scholar
Pottier, F. (2007b). Static name control for FreshML. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society, pp. 356–365.Google Scholar
Pouillard, N. & Pottier, F. (2010). A fresh look at programming with names and binders. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 217–228.Google Scholar
Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnia, R. (2010). Ott: Effective tool support for the working semanticist. J. Funct. Program. 20, 71–122.Google Scholar
Shinwell, M. R., Pitts, A. M. & Gabbay, M. J. (2003). FreshML: Programming with binders made simple. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, ICFP '03, pp. 263–274. New York, NY, USA: ACM.Google Scholar
Urban, C. (2008). Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40 (4), 327–356.Google Scholar
Weirich, S., Yorgey, B. A. & Sheard, T. (2011). Binders unbound. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 333–345.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.