Fall 2025 Seminars

Fall 2025

Organizer: Nicholas Coltharp

All Talks

Date Title Speaker
First-Order Reasoning about Laziness Anton Lorenzen
From Theory to Throughput: Evolving Datalog’s Semantics and Implementation Kristopher Micinski
Finite Choice Logic Programming Michael Arntzenius, Chris Martens
(WIP) Dijkstra monads for incorrectness logic Yao Li

First-Order Reasoning about Laziness

Speaker: Anton Lorenzen

Anton Lorenzen is pursuing a PhD in programming languages at the University of Edinburgh, where he is supervised by Sam Lindley and Daan Leijen. He has interned at the RiSE group of Microsoft Research and the OCaml compiler team of Jane Street, where he worked on Koka and modal uniqueness types. He holds a BSc in Mathematics and an MSc in Computer Science from the University of Bonn, Germany.

Lazy data structures have important properties in theory, but their adoption in practice has been limited. Part of the issue seems to be the difficulty of reasoning about them: laziness is opaque, which makes it hard to understand when thunks are evaluated. This is true even in a strict language, where laziness is tightly controlled. Furthermore, the amortized complexity analysis of lazy data structures typically uses debits instead of the more familiar credits. In this talk, I will present an alternative, first-order implementation of laziness which avoids these issues. This implementation allows us to defunctionalise lazy thunks and thus inspect what a thunk computes and when it is evaluated. Furthermore, I’ll present credit passing style, a simplified, credit-based version of Okasaki’s debit passing style. Together, these techniques yield a reasoning style that mirrors the concrete, credit-based analysis usually done for strict data structures. This talk is based on the work [https://dl.acm.org/doi/10.1145/3747530](https://dl.acm.org/doi/10.1145/3747530) and [https://dl.acm.org/doi/10.1145/3759164.3759351](https://dl.acm.org/doi/10.1145/3759164.3759351).

From Theory to Throughput: Evolving Datalog’s Semantics and Implementation

Speaker: Kristopher Micinski

Kristopher Micinski is an assistant professor at Syracuse. His work spans various domains (PL, databases, systems), but united by focusing on compilers, program analysis, and automated reasoning. Since starting at Syracuse, he and his students (but primarily his students) have been working on high-performance Datalog engines, with the hopes of building highly-scalable engines for static analysis, graph analytics, reverse engineering, and similar kinds of reasoning workloads. In his spare time he does woodworking.

Datalog is a simple logic programming language consisting of Horn clauses over atomic constants. Compared to conventional logic programming languages (Prolog, MiniKanren, and λProlog), Datalog eschews search in favor of an obviously-monotonic, chain-forward semantics leading to a rich array of applications in program analysis, database theory, and knowledge representation. In this talk, I describe our efforts in building the next generation of state-of-the-art Datalog solvers, targeting both Datalog's expressivity and scalability. I first introduce Datalog and discuss Slog (VLDB '25), an extension of Datalog to first-class facts, wherein every fact is identified uniquely by an S-expression; this syntactically-trivial extension readily enables the transliteration of natural-deduction-style rules in a variety of systems (e.g., constructive logics, type systems, and structural abstract interpreters). Additionally, Slog's properties permit a massively-parallel implementation--we have implemented Slog on top of MPI, leveraging recent work in parallel relational algebra to scale Slog programs (e.g., context-sensitive points-to analysis, graph algorithms) to thousands of cores. Alongside this CPU-focused implementation, I will briefly present our group's work on GPU Datalog, powered by our GPU-backed relation representations using row-oriented (ASPLOS '25) and column-oriented (AAAI '25, ICS '25) strategies; our results show that these engines are very competitive versus state-of-the-art CPU-based Datalog engines: the H100 beats a modern AMD server chip by 45-200x. I conclude by remarking on our long-term vision in building the next generation of logic programming engines, which strive to marry richly-expressive logical specification with robust, high-performance implementation.

Finite Choice Logic Programming

Speakers: Michael Arntzenius, Chris Martens

Michael Arntzenius is a postdoc at UC Berkeley. His primary interest is programming language design, using types, denotational semantics, and implementation strategies as a guide. Lately his focus is on combining ideas from functional programming, logic programming, and database engines. Chris Martens is an associate professor at Northeastern University. They are interested in elegant computational abstractions that support creative practices, in particular, in representing and reasoning about rule systems, such as game mechanics, privacy policies, procedural generation systems, and inference rules in PL metatheory. Their weapon of choice is the deep relationship between constructive logics and computation, via (1) logic programming and (2) type systems.

Logic programming lets us solve problems using logic: we write if-then rules and compute what they imply. For instance, "can this node reach this other node in this graph?" This is logical deduction: what MUST be true from certain assumptions & rules? SAT solving also lets us solve problems using logic: we write formulae and compute what satisfies them. For instance, "what are the 4x4 maps where each cell is a mountain, forest, or sea, and there are no seas next to mountains"? This is constrained choice: what COULD be true, subject to these constraints? Both of these have weaknesses: for instance, logic programming cannot easily express an arbitrary choice between mountain, forests, or sea, while SAT solving cannot easily express graph reachability. In this talk, we'll see how to combine choice and deduction into one system, Finite Choice Logic Programming, and explore a particular implementation of it, Dusa.

(WIP) Dijkstra monads for incorrectness logic

Speaker: Yao Li

Yao Li (He/Him) is an assistant professor of computer science at Portland State University. His main research area is in functional programming, interactive theorem proving, and program verification. His current research focuses on using interactive theorem provers to verify existing programs written without verification in mind. Some of his past work includes the verification of the DeepSpec web server and the verification of Haskell's containers library (using hs-to-coq). He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich. Before that, he obtained a MS degree and a BS degree from Shanghai Jiao Tong University in 2016 and 2013, respectively.

Dijkstra monads are monad-like structures that have been used in theorem provers like F* for specifying and verifying programs with effects, and they enable Hoare-style reasoning. The Dijkstra Monads for Free and Dijkstra Monads for All papers further propose a formal definition of these structures as a relation between a specification monad and an observation over a computation monad. But can we use Dijkstra monads for the new popular incorrectness logic? How does the theoretical model of Dijkstra monads framework work with incorrectness logic? In this talk, I will talk about my current exploration on this topic. It will be very much work-in-progres.