Jonathan Sterling

Harrison Grodin, Yue Niu, Jonathan Sterling et al. · cmu

We present Decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like Calf, the language is based on an internal phase distinction between the behavior of a program and its cost measured by an effect. Decalf extends Calf by accommodating other effects, such as probabilistic choice, which requires a reformulation of Calf's approach to cost analysis: rather than rely on a separable notion of cost, here a cost bound is simply another program. Formally, every type is equipped with an intrinsic preorder, allowing effectful programs to be compared for cost inequality. This approach serves as a streamlined alternative to the standard method of isolating a cost recurrence and readily extends to higher-order, effectful programs. The development proceeds by first introducing the Decalf type system, which is based on an intrinsic cost ordering among terms that restricts in the behavioral phase to extensional equality. This formulation is then applied to illustrative examples, including pure and effectful sorting algorithms. Finally, Decalf is semantically justified via a model in the topos of augmented simplicial sets.

Andrew Slattery, Jonathan Sterling

In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe from the category of sets into the category of set-valued presheaves on a small category. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the categorical nerve, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, the categorical nerve's functorial action on the universal small discrete fibration gives the generic family of the universe's Hofmann-Streicher lifting. Inspired by Awodey's analysis, we define a relative version of Hofmann-Streicher lifting in terms of the right pseudo-adjoint to the 2-functor given by postcomposition with a fibration. Finally, we construct a new 2-bifibration of fibrations in which the opcartesian and cartesian lifts arise from these pseudo-adjunctions.

Fredrik Bakke, Jonathan Sterling, Mark Damuni Williams et al.

In domains, categories, and toposes, the Sierpiński cone construction glues onto a space a universal closed point lying below all the other points. Although this is a lax colimit, it also enjoys a well-known right-handed universal property: the Sierpiński cone classifies partial maps defined on an open subspace. The situation proves more subtle in synthetic models of space based on extending homotopy type theory with an interval, as in several recent approaches to synthetic higher categories and domains: although globally it may well be the case that the Sierpiński cone classifies partial maps, this property cannot hold of all parameterised types without degenerating the theory. On the other hand, there are reflective subuniverses within which the classifying property nonetheless holds. We show that the largest subuniverse in which the Sierpiński cone classifies partial maps is the accessible localisation at a family of embeddings parameterised in the interval, and this subuniverse is contained within the Segal types; this containment is moreover strict in the sense that when the interval is non-trivial, it is not possible for all Segal types to lie in the subuniverse. We finally extend these results from Sierpiński cones to mapping cylinders, providing a new right-handed universal property for the latter.

Darryl McAdams, Jonathan Sterling

This paper proposes the use of dependent types for pragmatic phenomena such as pronoun binding and presupposition resolution as a type-theoretic alternative to formalisms such as Discourse Representation Theory and Dynamic Semantics.