Hendrik van Antwerpen
Casper Bach Poulsen
Eelco Visser
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.
Supplemental Material
- Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. 1991. Explicit Substitutions. Journal of Functional Programming 1, 4 (1991), 375–416.Google Scholar
Cross Ref
- Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.), Vol. 9600. Springer, 249–272.Google Scholar
- Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 666–679. Google ScholarDigital Library
- Luca Cardelli. 1988. Structural Subtyping and the Notion of Power Type. In POPL. 70–79. Google ScholarDigital Library
- Stephen Chang, Alex Knauth, and Ben Greenman. 2017. Type systems as macros. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 694–705. Google ScholarDigital Library
- Luís Damas and Robin Milner. 1982. Principal Type-Schemes for Functional Programs. In POPL. 207–212. Google ScholarDigital Library
- Torbjörn Ekman and Görel Hedin. 2006. Modular Name Analysis for Java Using JastAdd. In Generative and Transformational Techniques in Software Engineering, International Summer School, GTTSE 2005, Braga, Portugal, July 4-8, 2005. Revised Papers (Lecture Notes in Computer Science), Ralf Lämmel, João Saraiva, and Joost Visser (Eds.), Vol. 4143. Springer, 422–436.Google Scholar
- Torbjörn Ekman and Görel Hedin. 2007. The JastAdd extensible Java compiler. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr. (Eds.). ACM, 1–18. Google ScholarDigital Library
- Charles M. Ellison III. 2008. A Rewriting Logic Approach to Defining Type Systems. Master’s thesis. University of Illinois at Urbana-Champaign. http://hdl.handle.net/2142/18078 .Google Scholar
- Matthias Felleisen, Robby Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press. Google ScholarDigital Library
- Matthew Flatt. 2016. Binding as sets of scopes. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodik and Rupak Majumdar (Eds.). ACM, 705–717. Google ScholarDigital Library
- Thom Frühwirth. 2009. Constraint Handling Rules. Cambridge University Press.Google Scholar
- Thom Frühwirth and Pascal Brisset. 1995. High-Level Implementations of Constraint Handling Rules. Technical Report ECRC-TR-95-20.Google Scholar
- Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. Dissertation. Université Paris 7.Google Scholar
- Görel Hedin. 2009. An Introductory Tutorial on JastAdd Attribute Grammars. In Generative and Transformational Techniques in Software Engineering III - International Summer School, GTTSE 2009, Braga, Portugal, July 6-11, 2009. Revised Papers (Lecture Notes in Computer Science), Joao M. Fernandes, Ralf Lämmel, Joost Visser, and João Saraiva (Eds.), Vol. 6491. Springer, 166–200. Google ScholarDigital Library
- Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc 146 (December 1969).Google Scholar
- Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23, 3 (2001), 396–450. Google ScholarDigital Library
- Lennart C. L. Kats, Rob Vermaas, and Eelco Visser. 2011. Testing domain-specific languages. In Companion to the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011, Cristina Videira Lopes and Kathleen Fisher (Eds.). ACM, 25–26. Google ScholarDigital Library
- Lennart C. L. Kats and Eelco Visser. 2010. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, William R. Cook, Siobhán Clarke, and Martin C. Rinard (Eds.). ACM, Reno/Tahoe, Nevada, 444–463. Google ScholarDigital Library
- Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. 2016. Needle & Knot: Binder Boilerplate Tied Up. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science), Peter Thiemann (Ed.), Vol. 9632. Springer, 419–445.Google Scholar
- Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, and Li yao Xia. 2017. Beginner’s luck: a language for property-based generators. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 114–129. Google ScholarDigital Library
- Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. Syst. Sci. 17, 3 (1978), 348–375.Google ScholarCross Ref
- Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. 2014. Lem: reusable engineering of real-world semantics. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 175–188. Google ScholarDigital Library
- Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. 2015. A Theory of Name Resolution. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science), Jan Vitek (Ed.), Vol. 9032. Springer, 205–231.Google Scholar
- Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. TAPOS 5, 1 (1999), 35–55. Google ScholarDigital Library
- Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored local type inference. In POPL. 41–53. Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, Massachusetts. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Transactions on Programming Languages and Systems 22, 1 (2000), 1–44. Google ScholarDigital Library
- François Pottier and Diddier Rémy. 2005. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, 389–489.Google Scholar
- Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. 2016. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy (LIPIcs), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik.Google Scholar
- Casper Bach Poulsen, Arjen Rouvoet, Andrew P. Tolmach, Robbert Krebbers, and Eelco Visser. 2018. Intrinsically-typed definitional interpreters for imperative languages. PACMPL 2, POPL (2018). Google ScholarDigital Library
- John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974 (Lecture Notes in Computer Science), Bernard Robinet (Ed.), Vol. 19. Springer, 408–423. Google ScholarDigital Library
- Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397–434.Google ScholarCross Ref
- Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 359–374.Google Scholar
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. 2010. Ott: Effective tool support for the working semanticist. Journal of Functional Programming 20, 1 (2010), 71–122. Google ScholarDigital Library
- Vincent Simonet and François Pottier. 2007. A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems 29, 1 (2007), 1. Google ScholarDigital Library
- Paul Stansifer. 2016. Flexible binding-safe programming. Ph.D. Dissertation. Northeastern University.Google Scholar
- Rok Strnisa and Matthew J. Parkinson. 2011. Lightweight Java. Archive of Formal Proofs 2011 (2011).Google Scholar
- Martin Sulzmann and Peter J. Stuckey. 2008. HM(X) type inference is CLP(X) solving. Journal of Functional Programming 18, 2 (2008), 251–283. Google ScholarDigital Library
- Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. 2016. A constraint language for static semantic analysis based on scope graphs. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Martin Erwig and Tiark Rompf (Eds.). ACM, 49–60. Google ScholarDigital Library
- Dimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X) Modular type inference with local assumptions. J. Funct. Program. 21, 4-5 (2011), 333–412. Google ScholarDigital Library
Index Terms
- Scopes as types
Recommendations
Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications
There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to ...
Intrinsically-typed definitional interpreters for imperative languages
A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a ...
Practical pluggable types for java
ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysisThis paper introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the ...
Comments