Person. Steven Schaefer
I study the design and implementation of intrinsically correct software. In a sufficiently rich type system, a program’s type signature alone can carry a proof that it behaves as specified.
I am especially interested in verified compiler frontends, where parsing and typechecking algorithms can be built correct-by-construction.
Outside of research, I like to bake, garden, climb, play chess and play Tetris. Please send me a challenge in either (or anything else for that matter).
Papers
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsers
We present Dependent Lambek Calculus (Lambek), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.
We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
Talks
Lessons from Mechanizing Categorical Logic in Cubical Agda onpls-2026-talk
cubical-categorical-logic, a library of formalized category theory in Cubical Agda. The library’s core idea is to treat syntax as a free categorical structure whose dependent eliminator is stated via (displayed) universal properties. From the same reusable components we have proven canonicity and conservativity results across several type theories, as well as the coherence theorem for monoidal categories. In this talk, we discuss these applications and reflect on Cubical Agda as a host for mechanized metatheory, where it is sometimes a boon and sometimes a bane.Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus pldi-2025-talk
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In Dependent Lambek Calculus, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.
We present a denotational semantics of our type theory that interprets the types as a mathematical notion of formal grammars. Based on this denotational semantics, we have made a prototype implementation of Dependent Lambek Calculus using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus mwpls-2024-talk
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In Dependent Lambek Calculus, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.
We present a denotational semantics of our type theory that interprets the types as a mathematical notion of formal grammars. Based on this denotational semantics, we have made a prototype implementation of Dependent Lambek Calculus using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
LLL Algorithm lll-algorithm-video
Lenstra-Lenstra-Lovasz (LLL) Lattice Basis Reduction Algorithm. A very useful algorithm for computational number theory.
Final project for M602 Algebraic Number Theory at Indiana University.
Special thanks to Grant Sanderson for creating the manim library, and to Jeff Suzuki for illuminating videos on the algorithm!