Proving functional correctness of monadic programs using separation logic

Interaction trees are an active development in representing effectful and impure pro- grams in the Coq proof assistant. Examples of programs they can represent are programs that use: mutable state, concurrency and general recursion. Besides representing these programs we also want to reason about and verify these programs using separation logic....

Verifying the Semantics of Disambiguation Rules: Using Parse Tree Repairing for Showing Safety and Completeness of Associativity and Priority Rules

Context-free grammars (CFGs) provide a well-known formalism for the specification of programming languages. They describe the structure of a program in terms of parse trees. One major issue of CFGs is ambiguity, where one sentence can sometimes have multiple different parse trees. Some formalisms like SDF3 or YACC allow annotating a grammar with...

A type system for dynamic instances

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...

Cryostat Control: Real time control for a cryogenic refrigerator

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...