Abstract: Recently scope graphs were introduced as a formalism to specify the name binding structure of a program and do name resolution independent of the abstract syntax tree of a program. In this thesis we show how to use a constraint language based on scope graphs to do static analysis of programs. We do this by extracting constraints from a program, that specify name binding and typing. We treat binding and typing as separate building blocks, but our approach allows language constructs – such as access of record fields – where name and type resolution are mutually dependent. By using scope graphs for name resolution, our approach supports a wide range of name binding patterns that are not easily supported in existing constraint-based approaches. We present a formal semantics for our constraint language, as well as a solver algorithm, for which we discuss soundness, termination and completeness of the solver. We evaluate our approach by expressing the static semantics of PCF and Featherweight Java with our constraints, and we implemented the solver algorithm, as well as static analysis for both languages, in the Spoofax language workbench.
SERG is looking to strengthen its Programming Languages research program under the leadership of Prof. Dr. Eelco Visser. We aim at a broad program connecting logic, programming languages, and software engineering in order to improve the correctness, reliability, and security of software by using high-level, domain-specific formal specifications supported by tools such as certified compilers, model checkers, SMT solvers, and/or proof assistants. To that end, we are looking for an assistant professor to complement our current research strengths in language engineering and domain-specific languages with expertise in one or more of the following topics
On July 13 I gave a hands-on tutorial on language definition with Spoofax at the Summer School on DSL Design and Implementation at EPFL in Lausanne. Here is the original abstract and the recordings of the execution of the tutorial.
Language workbenches are tools aiming to reduce the gap between the design and implementation of (external domain-specific) programming languages. Given high-level descriptions of the syntax and semantics of a language, a workbench generates an implementation of an IDE and/or execution engine. There are many different approaches to realising these goals. In this session I will demonstrate and discuss the state of declarative language definition in the Spoofax Language Workbench.
In the first part of the session I give a hands-on tutorial of the development of language front-ends with Spoofax. We will explore syntax definition in SDF3, name binding and scope rules in NaBL, and type constraints in TS. Participants are expected to bring a (decently equipped) laptop with Eclipse/Spoofax and the exercise projects pre-installed according to the instructions provided at http://declare-your-language.metaborg.org/.
In the second part I will present recent research in expanding declarative language definition. (1) In our ESOP15 paper we develop a theory of name resolution to provide a generalisation and post-hoc semantics of the concepts of the NaBL name binding language. I will present the scope graph model, its resolution calculus, and the application of scope graphs to model name binding patterns in existing languages. (2) Language workbenches typically employ code generation to give semantics to languages. This often leads to questions about the exact source-level semantics of the language. We are working on DynSem, a DSL for the specification of dynamic semantics aimed at rapid prototyping, generation of interpreters, and (eventually) verification of soundness properties. DynSem is based on the work of implicitly modular operational semantics of Peter Mosses. I will discuss the current state of the design of the language.
Unfortunately, the sound is missing in the second half of the second video.
If you missed this tutorial, there will be a new (updated) edition at POPL 2016 in St Petersburg, Florida on Monday, January 18, 2016.
The program of a large conference such as SPLASH can be rather overwhelming. It is easy to get lost in the large number of talks. And even when you go through the program before the conference, you may not remember your selection while there. So, to help with that, we added support for personal schedules to the application, which should be useful to you if you’ll be attending any of the conferences hosted on researchr. We think the feature is pretty easy to use; click the star icon of any talks you’d like to attend and select ‘Your Program’ to see your selection. I have created a short video to demonstrate the new feature.