Abstract interpretation is a way of approximating the semantics of a computer program, in which we derive properties of those programs without actually performing the necessary computations for running the program, through the use of an abstract interpreter. To be able to trust the result of the abstract interpretation, we would to able to prove the soundness of the approximations of the interpreter. Previous work by Keidel et al. has shown that the soundness proofs of an entire abstract interpreter can be simplified by decomposing the interpreter by implementing concrete and abstract interpreters as instantiations of a generic interpreter. The goal of this thesis is to explore and implement mechanical proofs of soundness of such interpreters. To this end, we have used the interactive proof assistant Coq to implement a generic interpeter for a simple imperative language and instantiate it both concrete and abstract versions. The abstract interpreter is automatically proven sound via the use of Coq's automatic proof capabilities and typeclass system. Both the interpreted language and the used abstractions can be expanded to allow for more features. Soundness proofs can then be written for just the new components, those proofs will then be automatically resolved by Coq.

Statix is a language which generates a type checker from a declarative specification. However, Statix is not fast enough for quick feedback in IDEs because it always has to reanalyze all files. In this thesis, we improve the analysis time of Statix by applying the ideas of separate compilation to create a model for incremental analysis. Statix uses a scope graph for representing the scoping and declarations of a project. We split the scope graph over multiple smaller modules which can be analyzed in isolation. Our model automatically detects dependencies between modules and supports creating scope graph diffs to determine modules affected by changes with high precision. The modules from our model can be solved in parallel, already yielding performance improvements of up to 40% compared to the original implementation. Finally, we implement an optimistic strategy with our model and show that it is effective whenever changes are small, reducing analysis time by up to 5 times for large projects.

Since its inception in 1995, JavaScript usage has grown far beyond its initial domain of interactive websites. As the size of applications developed in the language grows, so does the desire for static analysis such as typechecking to provide safety and reliability. Many developments have been made in recent years on increasing the precision of analysis of JavaScript. This work introduces a concrete and a type interpreter for LambdaJS implemented within the Sturdy framework. The goal of this work is to evaluate the feasibility of implementing a shared interpreter using the Sturdy framework, evaluate the correctness of the concrete interpreter, and evaluate the feasibility of proving the typechecker sound. The resulting interpreters are tested experimentally with two test suites. The experimental evaluation gives confidence in the correctness of the concrete and abstract interpreter. A small part of the abstract interpreter is proven sound to evaluate the difficultyofcreatingacompletesoundnessproof.Thesuccessful implementation of the interpreters shows that implementing a shared arrow-based interpreter within the Sturdy framework is feasible for languages with complex semantics, that the utilities available reduce the effort required to do so, and that proving the abstract interpreter sound is simplified by using the library.

When using an integrated development environment, it is desirable to get real-time feedback on the correctness of the program. That is, we want to see the results of the type checker in real-time. However, type checking can take a long time, especially when the subject program is large. To be able to provide real-time results, we need to incrementalize the type checker. This way, when a program changes, we only need to recalculate results for the changed portion of the program, and everything that depends on it. In this thesis, we discuss how we used IncA to implement a type checker for Rust. IncA is a domain specific language for the definition of incremental program analyses: analyses written in IncA are automatically incrementalized. We show in our evaluation that our type checker updates results significantly faster than its non-incremental counterpart. While we were able to successfully implement many of Rust's features, there are some parts we were unable to implement, and we show why that is the case.

In this thesis, we focus on database query processing for so-called experience items, i.e., items commonly encountered in E-Commerce systems such as books, games or movies which are better described by their perceived subjective consumption experience, or Perceptual Features, than by factual meta-data normally used in SQL-style queries. To realize this, the perceived consumption experiences are extracted from social media feedback, like reviews or ratings, using methods such as Aspect-based Review Extraction or Document Embedding. These are then encoded either explicitly or implicitly as database tuples. We group similar tuples together for every item and determine the representative tuple for each of the groups, which are used in the Query-by-Example paradigm to allow users to explore and query the item space in an interactive and intuitive fashion.

In contrast to previous approaches with similar goals, like the article on ‘Exploiting Perceptual Similarity: Privacy-Preserving Cooperative Query Personalization by Lofi and Nieke’, we now introduce the notion of Shared Perspectives: paying respect to the subjectivity of user experiences. We do not try to encode only a single summarized experience for each item, but find and store dominant opinions shared by large parts of the user base instead. This allows us to represent controversial or split opinions much more accurately than previous systems, so the user can select which opinion is more relevant for them to find a similar item. We introduce the relevant conceptual foundations for Shared Perspectives, and give an overview of the design space for implementation. Furthermore, we showcase a prototype system, and evaluate it with respect to query performance as compared to previous approaches not featuring Shared Perspectives. We also investigate their semantic quality in a limited user study. As a result of these evaluations, we identify and resolve the new challenge of relevance of Perspectives, since not each commonly shared opinion is equally important or beneficial for query processing.