Side-effect are ubiquitous in programming. Examples include mutable state, exceptions, non-determinism, and user input. Algebraic effects and handlers are an approach to programming that gives a structured way of programming with effects. Each effect in a system with algebraic effects is defined by a set of operations. These operations can then be called anywhere in a program. Using a handler we can give an interpretation for the operations used. Unfortunately we are unable to express dynamic effects using regular algebraic effects, such as the dynamic creation of mutable references. Extending algebraic effects with effect instances enables us to express dynamic effects. These effect instances can be dynamically created and operations called on them are distinct from the same operation called on a different instance. Without a type system effect instances may result in runtime errors, because operation calls may be left unhandled. Because of their dynamic nature it is hard to give a type system for effect instances. In this thesis we present a new language, Miro, which extends algebraic effects and handlers with a restricted form of effect instances. We introduce the notion of an effect scope which encapsulates the creation and usage of dynamically created effect instances. We give a formal description of the syntax and semantics of Miro. We also give a type system which ensures that all operation calls are handled, so that there will be no runtime errors because of unhandled operation calls. Because effect instances can still escape their effect scope, in computationally irrelevant parts, we encounter difficulties in proving type safety for Miro. We discuss these difficulties and give a possible approach to prove type safety in the future.

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.

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.

A definitional interpreter is an interpreter which uses the semantics of its own host language to define those of its object language. Traditionally, a seperate type safety proof is used for such an interpreter. Using a "typesafe-by-construction" approach, where the typesafety is proven by expressing the type system of the object language in the type system of the host language is a new approach recently used for imperative languages. In this paper a proof-of-concept is made to show that the technique of "typesafe-byconstruction" can be also applied to interpreters for languages with explicit deallocation. This is done by making such an interpreter for a language called ML-dealloc, which is a basic version of ML extended with explicit allocation and deallocation. The interpreter is written in agda, which type system can be used to express ML-dealloc.

Technolution is a company that specializes in building embedded and information systems, in which software plays a key role. Recently, Technolution is transitioning from the use of C in embedded systems, to Rust, a relatively new programming language developed by Mozilla. By design, Rust provides the programmer with higher security and reliability guarantees, such as memory safety, type safety and the absence of race conditions. These guarantees are ensured by means of an expressive ownership-based type system. However, it is impossible for the Rust type system to detect all errors statically. Hence, there are still many operations that contain dynamic checks to test for erroneous conditions. When such a check fails, an unrecoverable problem has been encountered and the current thread exits, this is called a panic in Rust. A panic causes the program to terminate, leading to a decrease in availability of the system. To avoid situations causing panic, Technolution wants tooling that detects possible ways a program could panic. For this purpose, we developed a static analysis tool: Rustig. When given a program, Rustig notifies the user of all the operations that either directly, or indirectly via another library, may cause a panic. The tools performs the analysis of panic calls in two stages. First, it builds a call graph from the executable of a Rust program, modelling functions as nodes and function calls as directed edges. Secondly, it performs an analysis on the call graph to determine which functions could cause panic. As part of the development of Rustig, we devised two new approaches. We have developed an approach to construct call graphs taking into account dynamic dispatch calls. This is based upon the assumption once a function address is loaded, it will also be called during execution. Furthermore, in order to efficiently analyze the call graph, a simplification of the all paths problem is proposed. In contrast with the all paths problem, the simplification is solvable in polynomial time. The approach involves finding the shortest path for every crossing edge on a graph cut.

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.

In order to measure the spectrum of radio emissions from galaxies and other deep space objects, a new superconducting spectrometer, working at very cold temperatures close to the absolute zero, is developed. An advanced cooling system called a cryostat is used to cool down the spectrometer. The cool down of the cryostat involves the control of multiple sensors and actuators connected to the cryostat to achieve a final temperature below 250 millikelvin. A software program is used for this purpose. As extra hardware components have been added to the cryostat, the existing program does no longer fulfill the requirements. For this reason a new software program, which can monitor temperatures of all components and start control processes, is developed. The developed program consists of a client server structure. The server handles the logic of the cryostat using several controllers. It can send data to a native client, which is the graphical user interface, or a REST API. The native client displays sensor readouts received from the server and allows full control of server, which means it can start the cool down process as well as manual control processes. The REST API allows the user to have full control over the server using a Python script to achieve measurements which cannot be done from the native client. The increased automation, improved control and ability to integrate with external Python scripts allow the user to focus on the essential parts of an experiment making the developed program an improvement over the previous program.