Document Open Access Logo

Toward Semantic Foundations for Program Editors

Authors Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, Matthew A. Hammer

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.11.pdf
  • Filesize: 0.53 MB
  • 12 pages

Document Identifiers

Author Details

Cyrus Omar
Ian Voysey
Michael Hilton
Joshua Sunshine
Claire Le Goues
Jonathan Aldrich
Matthew A. Hammer

Cite AsGet BibTex

Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. Toward Semantic Foundations for Program Editors. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.SNAPL.2017.11

Abstract

Programming language definitions assign formal meaning to complete programs. Programmers, however, spend a substantial amount of time interacting with incomplete programs - programs with holes, type inconsistencies and binding inconsistencies - using tools like program editors and live programming environments (which interleave editing and evaluation). Semanticists have done comparatively little to formally characterize (1) the static and dynamic semantics of incomplete programs; (2) the actions available to programmers as they edit and inspect incomplete programs; and (3) the behavior of editor services that suggest likely edit actions to the programmer based on semantic information extracted from the incomplete program being edited, and from programs that the system has encountered in the past. This paper serves as a vision statement for a research program that seeks to develop these "missing" semantic foundations. Our hope is that these contributions, which will take the form of a series of simple formal calculi equipped with a tractable metatheory, will guide the design of a variety of current and future interactive programming tools, much as various lambda calculi have guided modern language designs. Our own research will apply these principles in the design of Hazel, an experimental live lab notebook programming environment designed for data science tasks. We plan to co-design the Hazel language with the editor so that we can explore concepts such as edit-time semantic conflict resolution mechanisms and mechanisms that allow library providers to install library-specific editor services.
Keywords
  • program editors
  • type systems
  • live programming
  • program prediction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Alfred V. Aho and Thomas G. Peterson. A minimum distance error-correcting parser for context-free languages. SIAM J. Comput., 1(4):305-312, 1972. URL: http://dx.doi.org/10.1137/0201022.
  2. Luís Eduardo de Souza Amorim, Sebastian Erdweg, Guido Wachsmuth, and Eelco Visser. Principled syntactic code completion using placeholders. In Software Language Engineering (SLE), 2016. URL: http://dx.doi.org/10.1145/2997364.2997374.
  3. Dimitar Asenov and Peter Müller. Envision: A fast and flexible visual code editor with fluid interactions (Overview). In IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), 2014. Google Scholar
  4. Edwin Brady. Idris, A General-Purpose Dependently Typed Programming Language: Design and Implementation. Journal of Functional Programming, 23(05):552-593, 2013. Google Scholar
  5. Sebastian Burckhardt, Manuel Fahndrich, Peli de Halleux, Sean McDirmid, Michal Moskal, Nikolai Tillmann, and Jun Kato. It’s alive! continuous feedback in UI programming. In PLDI, 2013. URL: http://dx.doi.org/10.1145/2491956.2462170.
  6. Margaret M. Burnett, John W. Atwood Jr., and Zachary T. Welch. Implementing level 4 liveness in declarative visual programming languages. In IEEE Symposium on Visual Languages, 1998. Google Scholar
  7. Philippe Charles. A practical method for constructing efficient LALR (K) parsers with automatic error recovery. PhD thesis, New York University, 1991. Google Scholar
  8. Paul Chiusano. Unison. http://www.unisonweb.org/. Accessed: 2016-04-25.
  9. Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. Programmatic and direct manipulation, together at last. In PLDI, 2016. Google Scholar
  10. Matteo Cimini and Jeremy G. Siek. The gradualizer: a methodology and algorithm for generating gradual type systems. In POPL, 2016. Google Scholar
  11. Barthélémy Dagenais and Laurie J. Hendren. Enabling static analysis for partial Java programs. In OOPSLA, 2008. Google Scholar
  12. Maartje de Jonge, Emma Nilsson-Nyman, Lennart C. L. Kats, and Eelco Visser. Natural and flexible error recovery for generated parsers. In Software Language Engineering (SLE), 2009. Google Scholar
  13. Erich Gamma and Kent Beck. Contributing to Eclipse: principles, patterns, and plug-ins. Addison-Wesley Professional, 2004. Google Scholar
  14. Susan L. Graham, Charles B. Haley, and William N. Joy. Practical lr error recovery. ACM SIGPLAN Notices, 14(8), 1979. URL: http://dx.doi.org/10.1145/872732.806967.
  15. Sumit Gulwani. Dimensions in program synthesis. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'10, pages 13-24, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1836089.1836091.
  16. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Type classes in Haskell. ACM Trans. Program. Lang. Syst., 18(2):109-138, 1996. Google Scholar
  17. Abram Hindle, Earl T. Barr, Zhendong Su, Mark Gabel, and Premkumar Devanbu. On the naturalness of software. In International Conference on Software Engineering (ICSE), pages 837-847, 2012. Google Scholar
  18. James A. Jones, Mary Jean Harrold, and John Stasko. Visualization of test information to assist fault localization. In International Conference on Software Engineering (ICSE), pages 467-477, Orlando, FL, USA, 2002. URL: http://dx.doi.org/10.1145/581339.581397.
  19. Lennart C. L. Kats, Maartje de Jonge, Emma Nilsson-Nyman, and Eelco Visser. Providing rapid feedback in generated modular language environments: adding error recovery to scannerless generalized-LR parsing. In OOPSLA, 2009. URL: http://dx.doi.org/10.1145/1640089.1640122.
  20. Lennart C. L. Kats and Eelco Visser. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In OOPSLA, 2010. Google Scholar
  21. Yalin Ke, Kathryn T. Stolee, Claire Le Goues, and Yuriy Brun. Repairing programs with semantic code search. In International Conference On Automated Software Engineering (ASE), 2015. Google Scholar
  22. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. GenProg: A generic method for automatic software repair. IEEE Transactions on Software Engineering (TSE), 38:54-72, 2012. URL: http://dx.doi.org/10.1109/TSE.2011.104.
  23. Fan Long and Martin Rinard. Automatic patch generation by learning correct code. In POPL, 2016. URL: http://dx.doi.org/10.1145/2837614.2837617.
  24. Eyal Lotem and Yair Chuchem. Project Lamdu. http://www.lamdu.org/. Accessed: 2016-04-08.
  25. Conor McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics., 2000. Google Scholar
  26. Sean McDirmid. Living it up with a live programming language. In OOPSLA, 2007. Google Scholar
  27. Sean McDirmid. Usable live programming. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming &Software, Onward! 2013, 2013. Google Scholar
  28. Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In International Conference on Software Engineering (ICSE), 2016. Google Scholar
  29. Tom Murphy VII, Karl Crary, and Robert Harper. Type-safe distributed programming with ML5. In International Symposium on Trustworthy Global Computing, pages 108-123. Springer, 2007. Google Scholar
  30. Kıvanç Muşlu, Yuriy Brun, Reid Holmes, Michael D. Ernst, and David Notkin. http://people.cs.umass.edu/brun/pubs/pubs/Muslu12icse-nier.pdf. In New Ideas and Emerging Results Track at the 34th International Conference on Software Engineering (ICSE), 2012.
  31. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Trans. Comput. Log., 9(3), 2008. Google Scholar
  32. Ulf Norell. Dependently typed programming in agda. In Advanced Functional Programming, pages 230-266. Springer, 2009. Google Scholar
  33. Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. Safely composable type-specific languages. In ECOOP, 2014. Google Scholar
  34. Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew Hammer. Hazelnut: A bidirectionally typed structure editor calculus. In POPL, 2017. URL: https://arxiv.org/abs/1607.04180.
  35. Cyrus Omar, YoungSeok Yoon, Thomas D. LaToza, and Brad A. Myers. Active code completion. In International Conference on Software Engineering (ICSE), 2012. Google Scholar
  36. Fernando Pérez and Brian E. Granger. IPython: a system for interactive scientific computing. Computing in Science and Engineering, 9(3):21-29, May 2007. URL: http://ipython.org.
  37. Brigitte Pientka. Beluga: Programming with dependent types, contextual data, and contexts. In International Symposium on Functional and Logic Programming (FLOPS), 2010. URL: http://dx.doi.org/10.1007/978-3-642-12251-4_1.
  38. Yuhua Qi, Xiaoguang Mao, Yan Lei, and Chengsong Wang. Using automated program repair for evaluating the effectiveness of fault localization techniques. In International Symposium on Software Testing and Analysis, 2013. Google Scholar
  39. Manos Renieris and Steven Reiss. Fault localization with nearest neighbor queries. In IEEE/ACM International Conference on Automated Software Engineering (ASE), 2003. Google Scholar
  40. Mitchel Resnick, John Maloney, Andrés Monroy-Hernández, Natalie Rusk, Evelyn Eastmond, Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, and Yasmin Kafai. Scratch: Programming for All. Commun. ACM, 52(11):60-67, November 2009. URL: http://dx.doi.org/10.1145/1592761.1592779.
  41. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006. Google Scholar
  42. Simon Peyton Jones, Sean Leather and Thijs Alkemade. Typed holes in GHC. URL: https://wiki.haskell.org/GHC/Typed_holes.
  43. Steven L. Tanimoto. VIVA: A visual language for image processing. J. Vis. Lang. Comput., 1(2):127-139, 1990. URL: http://dx.doi.org/10.1016/S1045-926X(05)80012-6,
  44. Steven L. Tanimoto. A perspective on the evolution of live programming. In 1st International Workshop on Live Programming, (LIVE), 2013. Google Scholar
  45. Tim Teitelbaum and Thomas Reps. The Cornell Program Synthesizer: A Syntax-directed Programming Environment. Commun. ACM, 24(9):563-573, 1981. URL: http://dx.doi.org/10.1145/358746.358755.
  46. Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, and Manuel Fahndrich. TouchDevelop: Programming Cloud-connected Mobile Devices via Touchscreen. In SIGPLAN Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2011. URL: http://dx.doi.org/10.1145/2048237.2048245.
  47. Mark G. J. van den Brand, Arie van Deursen, Jan Heering, H. A. de Jong, Merijn de Jonge, Tobias Kuipers, Paul Klint, Leon Moonen, Pieter A. Olivier, Jeroen Scheerder, Jurgen J. Vinju, Eelco Visser, and Joost Visser. The ASF+SDF meta-environment: A component-based language development environment. In International Conference on Compiler Construction (CC), 2001. Google Scholar
  48. Paul Van Der Walt and Wouter Swierstra. Engineering proof by reflection in Agda. In Symposium on Implementation and Application of Functional Languages, 2012. Google Scholar
  49. Bret Victor. Inventing on principle. Invited talk, Canadian University Software Engineering Conference (CUSEC), 2012. Google Scholar
  50. Markus Voelter. Language and IDE Modularization and Composition with MPS. In International Summer School on Generative and Transformational Techniques in Software Engineering, pages 383-430. Springer, 2011. Google Scholar
  51. Markus Voelter, Daniel Ratiu, Bernhard Schaetz, and Bernd Kolb. Mbeddr: An Extensible C-based Programming Language and IDE for Embedded Systems. In SPLASH, 2012. URL: http://dx.doi.org/10.1145/2384716.2384767.
  52. Markus Voelter, Janet Siegmund, Thorsten Berger, and Bernd Kolb. Towards User-Friendly Projectional Editors. In Software Language Engineering (SLE), 2014. URL: http://dx.doi.org/10.1007/978-3-319-11245-9_3.
  53. Beta Ziliani, Derek Dreyer, Neelakantan R Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming, 25:e12, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact