What's new

From the blog

Changing the frame, part 1: Formal modeling with LLM assistance (9/18/2026)

Tools for formal modeling have so far favored generality and lack of constraints over well-adaptedness and safeguards. The emergence of LLMs is changing the balance by making it easier to create formal artifacts but harder to be confident in their reliability. Next-generation technology for formal modeling should meet this moment by situating models within more constrained frames, while enabling the frame to be fluidly shifted when circumstances demand.

Latest paper

Twisted double functors and loosely discrete opfibrations, 2026. Michael Lambert, David Jaz Myers, Evan Patterson.

We investigate notions of "loose module" or "loose copresheaf" over a double category: an action by the double category's loose morphisms. Two main models for loose copresheaves are introduced and compared, one based on twisted double functors—a new kind of double functor sending tight morphisms to loose morphisms and vice versa—and the other being loosely discrete opfibrations. We take the perspective that twisted copresheaves generalize indexed categories, putting the domain and codomain on an equal footing. Read more