At Topos we aim to build the next generation of formal languages for modeling and programming. Reflecting our roots as category theorists, we often take a “categories-first” approach to language design: we start by asking what categorical structure best captures the essential features of the phenomenon at hand. Category theory is a powerful tool for designing bespoke formal languages, as it allows new structures to be rapidly assembled from a library of well-tested and interoperable abstractions. Yet the categories-first approach leaves open the crucial questions of how to present and, ultimately, implement a formal language with the desired categorical semantics.
We seek a type theorist who will work closely with category theorists and research software engineers to design and implement new languages outside the standard paradigms of programming.
A few different projects, all at early stages of development, illustrate the work:
- Double-categorical logic is a meta-logic that is able to uniformly specify the categorical structures corresponding to a range of substructural logics, standard and not-so-standard. Can we then uniformly define and implement type theories for—internal languages of—these categorical structures?1
- Within double-categorical logic, the means of specifying a categorical logic is a double theory, a kind of (virtual) double category. Can we find and implement the internal languages of virtual double categories and related structures, like virtual equipments?2
- In biochemistry, rule-based models succinctly and declaratively specify reaction networks with combinatorially many species or reactions. A categorical semantics for a rule-based model that generalizes several existing tools is a symmetric monoidal indexed category, whose two levels correspond to patterns and rules. What is the (linear) type theory for this structure?3
A commonality among these projects is how taking categories and categorical logic seriously leads to exciting new challenges in type theory.
If you are a type theorist excited to work with a first-rate team of category theorists and research software engineers to design and build next-generation formal languages, please consider applying for this position as a Research Software Engineer in our Berkeley office:
Call for applications: CA-2026-RSE-1
Footnotes
This project is a collaboration with tslil clingman, based in the Topos UK office. So far, I’ve drafted a spec for this uniform type theory, available as CatColab RFC-0004, and tslil has built a prototype implementation.↩︎
This project is a collaboration with Bryce Goldman, building on work by Hayato Nasu. For an introduction, check out Bryce’s recent blog post.↩︎
This project is a collaboration with systems biologist Paul Lang, who was recently a visiting researcher at Topos. We haven’t written much about it yet, but we do have a work-in-progress implementation.↩︎