AZ
A.S. Zwaan
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
3 records found
1
Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition.
...
Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition.
The Statix meta-language has been developed in order to simplify the definition of static semantics in programming languages. A high-level static semantics definition of a language in Statix can be used to generate a type-checker, hence abstracting over the shared implementation details. Statix should be able to express the static semantics of itself as well. The process of defining a language using itself is called bootstrapping. In this thesis we discuss the bootstrapping of the Statix meta-language within the Spoofax language workbench. The bootstrapping of a type-system domain specific language hasn't previously been discussed in existing work. It acts as an interesting case study on the use of Statix to define semantics for a constraint-based declarative language as well as the use of Statix throughout a full compiler pipeline. In addition bootstrapping grants Statix a more expressive type system, which enables the future development of the language.
Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.
The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench. ...
Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.
The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench. ...
The Statix meta-language has been developed in order to simplify the definition of static semantics in programming languages. A high-level static semantics definition of a language in Statix can be used to generate a type-checker, hence abstracting over the shared implementation details. Statix should be able to express the static semantics of itself as well. The process of defining a language using itself is called bootstrapping. In this thesis we discuss the bootstrapping of the Statix meta-language within the Spoofax language workbench. The bootstrapping of a type-system domain specific language hasn't previously been discussed in existing work. It acts as an interesting case study on the use of Statix to define semantics for a constraint-based declarative language as well as the use of Statix throughout a full compiler pipeline. In addition bootstrapping grants Statix a more expressive type system, which enables the future development of the language.
Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.
The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench.
Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.
The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench.
Renaming for Everyone
Language-parametric Renaming in Spoofax
A refactoring is a program transformation that improves the design of the source code, while preserving its behavior. Most modern IDEs offer a number of automated refactorings as editor services. The Rename refactoring is the most-commonly applied refactoring and is used to change the identifier of a program entity such as a variable, a function, or a type. Correctly implementing refactorings is notoriously complex and these state-of-the-art implementations are known to be faulty and too restrictive. When developing a new programming language, it is both difficult and time-consuming to implement sound and complete automated refactoring transformations. Language-parametric definitions of refactorings that can be reused by instantiation with the syntax and semantics of a language, allow the development effort of refactorings to be amortized across language implementations. In this thesis, we developed a language-parametric Rename refactoring algorithm that works on an abstract model of a program's name binding structure. We implemented the algorithm in the Spoofax language workbench, building on the language-parametric representation of name binding with scope graphs and using generic traversals in the Stratego transformation language. We evaluated the algorithm with five different languages implemented in Spoofax, which uses both NaBL2 and Statix to declare their static semantics and name binding rules. As a result, Spoofax now provides an automated Rename refactoring that works for any language developed with the language workbench using NaBL2/Statix.
...
A refactoring is a program transformation that improves the design of the source code, while preserving its behavior. Most modern IDEs offer a number of automated refactorings as editor services. The Rename refactoring is the most-commonly applied refactoring and is used to change the identifier of a program entity such as a variable, a function, or a type. Correctly implementing refactorings is notoriously complex and these state-of-the-art implementations are known to be faulty and too restrictive. When developing a new programming language, it is both difficult and time-consuming to implement sound and complete automated refactoring transformations. Language-parametric definitions of refactorings that can be reused by instantiation with the syntax and semantics of a language, allow the development effort of refactorings to be amortized across language implementations. In this thesis, we developed a language-parametric Rename refactoring algorithm that works on an abstract model of a program's name binding structure. We implemented the algorithm in the Spoofax language workbench, building on the language-parametric representation of name binding with scope graphs and using generic traversals in the Stratego transformation language. We evaluated the algorithm with five different languages implemented in Spoofax, which uses both NaBL2 and Statix to declare their static semantics and name binding rules. As a result, Spoofax now provides an automated Rename refactoring that works for any language developed with the language workbench using NaBL2/Statix.