Patrick Bahr
YOU?
Author Swipe
The Calculated Typer (Functional Pearl) Open
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how …
Calculating Compilers Effectively (Functional Pearl) Open
Much work in the area of compiler calculation has focused on pure languages. While this simplifies the reasoning, it reduces the applicability. In this article, we show how an existing compiler calculation methodology can be naturally exte…
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl) Open
Bahr and Hutton recently developed an approach to compiler calculation that allows a wide range of compilers to be derived from specifications of their correctness. However, a limitation of the approach is that it results in compilers that…
Asynchronous Modal FRP Open
Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity and lack of space leaks. So far, almost all of these languag…
Calculating Compilers for Concurrency Open
Choice trees have recently been introduced as a general structure for defining the semantics of programming languages with a wide variety of features and effects. In this article we focus on concurrent languages, and show how a codensity v…
Asynchronous Modal FRP Open
Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity and lack of space leaks. So far, almost all of these languag…
Monadic compiler calculation (functional pearl) Open
Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers converging behaviour of the source language, which means that the…
Modal FRP for all: Functional reactive programming without space leaks in Haskell Open
Functional reactive programming (FRP) provides a high-level interface for implementing reactive systems in a declarative manner. However, this high-level interface has to be carefully reigned in to ensure that programs can in fact be execu…
Proceedings 11th International Workshop on Computing with Terms and\n Graphs Open
Graphs, and graph transformation systems, are used in many areas within\nComputer Science: to represent data structures and algorithms, to define\ncomputation models, as a general modelling tool to study complex systems, etc.\nResearch in …
Diamonds are not forever: liveness in reactive programming with guarded recursion Open
When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level of abstraction while ensuring that all programs can be impl…
Calculating correct compilers II: Return of the register machines Open
In ‘Calculating Correct Compilers’ (Bahr & Hutton, 2015), we developed a new approach to calculating compilers directly from specifications of their correctness. Our approach only required elementary reasoning techniques and has been used …
Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks Open
Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all progr…
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming. Open
Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all progr…
Convergence in infinitary term graph rewriting systems is simple Open
Term graph rewriting provides a formalism for implementing term rewriting in an efficient manner by emulating duplication via sharing. Infinitary term rewriting has been introduced to study infinite term reduction sequences. Such infinite …
Strict Ideal Completions of the Lambda Calculus Open
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions o…
Strict Ideal Completions of the Lambda Calculus Open
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions o…
The clocks are ticking: No more delays! Open
Guarded recursion in the sense of Nakano allows general recursive types and terms to be added to type theory without breaking consistency. Recent work has demonstrated applications of guarded recursion such as programming with codata, reas…
Böhm Reduction in Infinitary Term Graph Rewriting Systems Open
The confluence properties of lambda calculus and orthogonal term rewriting do not generalise to the corresponding infinitary calculi. In order to recover the confluence property in a meaningful way, Kennaway et al. introduced Böhm reductio…
Compiling a 50-year journey Open
Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a reg…