Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model.
Furthermore, they need to interact with other languages targeting said runtimes.
A language targeting only one runtim ...
Production compilers commonly perform dozens of transformations on an intermediate representation. Running those transformations in separate passes harms performance. One approach to recover performance is to combine transformations by hand in order to red ...
Compile-time metaprogramming has been proven immensely useful enabling programming techniques such as language virtualization, embedding of external DSLs, self-optimization, and boilerplate generation amongst many others. In the recent production release o ...
Type classes were originally developed in Haskell as a disciplined alternative to ad-hoc polymorphism. Type classes have been shown to provide a type-safe solution to important challenges in software engineering and programming languages such as, for examp ...