Lecture 6: Introduction to Static Analysis
In this lecture we discuss the need for type checking, or more broadly, static analysis, i.e. the application of analyses to the static representation (text, AST) of a program.
Topics
- Type checking
- Schema checking
- Defining type checkers
- Name binding
- Name resolution
- Scope graphs
Slides
Reading Material
-
Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser. Scopes as types. Proceedings of the ACM on Programming Languages, 2 (OOPSLA), 2018. This paper introduces Statix, a language for writing static semantics specifications.
-
Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Martin Erwig, Tiark Rompf, editors, Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pages 49-60, ACM, 2016. This paper develops a constraint language for description of type system using scope graph constraints for the definition of name binding. These constraints are the basis for the NaBL2 language.
-
Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. A Theory of Name Resolution. In Jan Vitek, editor, 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. Volume 9032 of Lecture Notes in Computer Science, pages 205-231, Springer, 2015. This paper introduces the scope graph model for the representation of name binding facts in programs and the resolution calculus to resolve names in scope graphs.
Additional Reading Material
- Gabriël Konat, Lennart C. L. Kats, Guido Wachsmuth, Eelco Visser. Declarative Name Binding and Scope Rules. In Krzysztof Czarnecki, Görel Hedin, editors, Software Language Engineering, 5th International Conference, SLE 2012, Dresden, Germany, September 26-28, 2012, Revised Selected Papers. Volume 7745 of Lecture Notes in Computer Science, pages 311-331, Springer, 2012. This paper introduces the NaBL language for describing the name binding rules of programming languages. This work inspired the development of the scope graph model.
Related Videos
Recording of a Curry On 2018 demonstration of SDF3 and NaBL2 to live develop syntax and type system of programming languages.
Recording of a Curry On 2017 talk about scope graphs