<p dir="ltr">This thesis explores two approaches to bridge the gap between expressiveness and performance in programming languages. It presents two complementary directions that reconcile performance and expressiveness: retrofitting static performance guarantees into an expressive general-purpose language like Scala, and transparently extending a restricted language like Datalog with features like polymorphism and user-defined functions while generating specialized and efficient code.</p><p dir="ltr">We first introduce storage modes, lightweight type qualifiers that enable statically tracking the lifetime of values in Scala programs. This enables stack allocating them and reduce memory pressure on the garbage collector. A key novelty is delaying the popping of the stack frames when returning dynamically-sized stack-allocated values, overcoming limitations of previous approaches.</p><p dir="ltr">Second, we present Flan, a Datalog compiler and embedding in Scala implemented as a multi-stage interpreter. Through staging, Flan can generate highly specialized code for different execution strategies and indexing structures, achieving performance on par with state-of-the-art domain-specific compilers like Soufflé. Moreover, by leveraging the host language, Flan enables seamless extension of Datalog with powerful features like user-defined functions, lattices and polymorphism, retaining the expressiveness of languages like Flix.</p><p dir="ltr">Overall, this work advances the design space for expressive and efficient programming languages, through lightweight annotations in an expressive host language, and transparent compiler specialization of an embedded domain-specific language. The techniques intoduced bridghe the gap between low-level performance and high-level programming abstractions.</p>

<p>Static program analyzers are vital tools to produce useful insights about programs without executing these programs. These insights can be used to improve the quality of programs, e.g., detecting defects in programs, or optimizing programs to use fewer resources. However, building static program analyzers that are simultaneously sound, performant, and flexible is notoriously challenging.</p> <p>This dissertation aims to address this challenge by exploring the potential of applying correct-by-construction metaprogramming techniques to build static program analyzers. Metaprogramming techniques manipulate and transform programs as data objects.  In this thesis, we consider static program analyzers as the objects to be manipulated or transformed. We show that metaprogramming techniques can improve our understanding, the construction, flexibility, and performance of program analyzers.</p> <p>We first study the inter-derivation of abstract interpreters. Using off-the-shelf program transformation techniques such as refunctionalization, we demonstrate that big-step abstract interpreters can be mechanically derived from their small-step counterparts, thus building a functional correspondence between two different styles of abstract interpretation.</p> <p>To build high-performance program analyzers, we exploit the first Futamura projection to build compilers for abstract interpretation and symbolic execution. The first Futamura projection states that specializing an interpreter with respect to an input program is a process equivalent to compilation, thus providing a practical way to repurpose interpreters for compilation and code generation. We systematically apply this idea to build program-analysis compilers by writing analyzers as staged interpreters using higher-level abstractions. The staged interpreter can be used for generating sound and performant analysis code given a specific input program. Moreover, the approach enables using abstractions without regret: by using higher-level program abstractions, the analyzer can be written in a way that is close to its high-level specification (e.g. big-step operational semantics), and by compilation, the analyzer is performant since it does not need to pay the runtime overhead of using these abstraction mechanisms.</p> <p>We also develop novel type systems that track sharing and separation in higher-order imperative languages. Such type systems are useful both for general-purpose programming languages and for optimization of domain-specific metaprograms such as those program-analysis compilers.</p> <p><br></p>

<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>