Programming language implementations bridge the gap between what the program developer sees and understands, and what the computer executes. Hence, it is crucial for the reliability of software that language implementations are correct. Correctness of an implementation is judged with respect to a criterion. In this thesis, we focus on the criterion type correctness, striking a balance between the difficulty of the assessment of the criterion and its usefulness to rule out errors throughout a programming language implementation. If both the front- and the back-end fulfill their role in maintaining the type contract between the programmer and the language implementation, then unexpected type errors will not occur when the program is executed. To verify type correctness throughout a language implementation, we want to establish it formally. That is, we aim to give a specification of program typing in a formal language, and to give a mathematical proof that every part of the language implementation satisfies the necessary property to make the whole implementation type-correct. Type checkers ought to be sound and only accept programs that are indeed typeable according to the specification of the language. Interpreters should be type safe, and reduce expressions to values of the same type. Program compilers should preserve well-typing when they transform programs. These properties are essential for implementations of typed programming languages, ensuring that the typing of the source program is a meaningful notion that can be trusted by the programmer to prevent certain errors from occurring during program execution. A conventional formal type-

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.

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.

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.

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.