Cartesius is a semantic model for defining expressive n-way joins/merges over asynchronous event sequences/streams. Joins exists in different domains, e.g., stream-relational algebra, complex event patterns, (functional) reactive programming and concurrent programming (join calculus). With Cartesius, we can define join variants in a uniform and structured manner. We may think of Cartesius as solving an instance of Wadler's "expression problem" in the realm of big data. The workhorse are algebraic effects and handlers, which we employ to interpret declarative join pattern specifications in different ways.
PolyJoin complements Cartesius with a pragmatic, type-safe, and purely combinator-based programming language embedding of comprehension syntax for joins. It permits more liberal notions of computations than LINQ, respectively monadic "do" and "for" comprehensions.
Code: github References: [Bračevac 2019] [Bračevac et al. 2018] [Bračevac et al. 2019]
A principled and performant approach to constructing symbolic execution engines and symbolic compilers, which has been considered hard -- until now! We combine programming language's vanilla definitional interpreter, algebraic effects and handlers, multi-stage programming, and the first Futamura projection.
Code: github References: [Wei et al. 2020]
Explores how we may systematically obtain an *incremental* type checker for a given programming language. Incrementalization avoids expensive re-computation of type checking and other program analyses in large-scale software projects and thus may lower the latency in IDEs and decrease compilation times overall. The project is based on the notion of *co-contextual* typing rules.
Code: github References: [Erdweg et al. 2015] [Kuci et al. 2017]
Explores foundations of typed distributed programming with first-class server abstractions, join patterns for synchronization, and transparent placement. Server configurations, deployments, and cloud/middleware services can be programmed as libraries of combinators in CPL. These tasks usually require a multitude of unsafe configuration languages with no safety net. Comes with an interpreter in Scala and a PLT Redex mechanization.
Code: github References: [Bračevac et al. 2016]