Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.

We consider the problem of constructing the free bifibration generated by a functor of categories $𝑝:𝐷\to 𝐶$. This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Paré, and Pronk, of “freely adjoining adjoints” to a category. We develop a proof-theoretic approach to the problem, beginning with a construction of the free bifibration ${\mathrm{\Lambda }}_{𝑝}:𝐵𝑖𝑓𝑖𝑏(𝑝)\to 𝐶$ in which objects of $𝐵𝑖𝑓𝑖𝑏(𝑝)$ are formulas of a primitive “bifibrational logic”, and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence. We show that instantiating the construction to the identity functor generates a _zigzag double category_ $\mathbb{Z}(𝐶)$, which is also the free double category with companions and conjoints (or fibrant double category) on $𝐶$. The approach adapts smoothly to the more general task of building $(𝑃,𝑁)$-fibrations, where one only asks for pushforwards along arrows in $𝑃$ and pullbacks along arrows in $𝑁$ for some subsets of arrows; this encompasses Kock and Joyal’s notion of _ambifibration_ when $(𝑃,𝑁)$ form a factorization system. We establish a series of progressively stronger normal forms, guided by ideas of _focusing_ from proof theory, and obtain a canonicity result under assumption that the base category is factorization preordered relative to $𝑃$ and $𝑁$. This canonicity result allows us to decide the word problem and to enumerate relative homsets without duplicates. Finally, we describe several examples of a combinatorial nature, including a category of plane trees generated as a free bifibration over $𝜔$, and a category of increasing forests generated as a free ambifibration over $\mathrm{\Delta }$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition for bicartesian squares.

We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows $\mathrm{𝒲︀}\mathrm{𝒞︀}$ for any category $\mathrm{𝒞︀}$. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without $𝜖$-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor $\mathrm{𝒲︀}:\text{Cat}\to \text{Oper}$ admits a left adjoint $\mathrm{𝒞︀}:\text{Oper}\to \text{Cat}$, which we call the contour category construction since the arrows of $\mathrm{𝒞︀}\mathrm{𝒪︀}$ have a geometric interpretation as oriented contours of operations of $\mathrm{𝒪︀}$. A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset $𝐿\subseteq \mathrm{𝒞︀}(𝐴,𝐵)$ is a CFL of arrows if and only if it is a functorial image of the intersection of a $\mathrm{𝒞︀}$-chromatic tree contour language with a regular language.

We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.

We present ${𝜆}_{\text{ert}}$, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4.

Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google’s pKVM hypervisor for Android.

We begin by explaining how any context-free grammar encodes a functor of operads from a freely generated operad into a certain “operad of spliced words”. This motivates a more general notion of CFG over any category $𝐶$, defined as a finite species $𝑆$ equipped with a color denoting the start symbol and a functor of operads $𝑝:𝐹𝑟𝑒𝑒[𝑆]\to 𝑊[𝐶]$ into the operad of spliced arrows in $𝐶$. We show that many standard properties of CFGs can be formulated within this framework, and that usual closure properties of CF languages generalize to CF languages of arrows. We also discuss a dual fibrational perspective on the functor $𝑝$ via the notion of “displayed” operad, corresponding to a lax functor of operads $𝑊[𝐶]\to 𝑆𝑝𝑎𝑛(𝑆𝑒𝑡)$.

We then turn to the Chomsky-Schützenberger Representation Theorem. We describe how a non-deterministic finite state automaton can be seen as a category $𝑄$ equipped with a pair of objects denoting initial and accepting states and a functor of categories $𝑄\to 𝐶$ satisfying the unique lifting of factorizations property and the finite fiber property. Then, we explain how to extend this notion of automaton to functors of operads, which generalize tree automata, allowing us to lift an automaton over a category to an automaton over its operad of spliced arrows. We show that every CFG over a category can be pulled back along a ND finite state automaton over the same category, and hence that CF languages are closed under intersection with regular languages. The last important ingredient is the identification of a left adjoint $𝐶[-]:𝑂𝑝𝑒𝑟𝑎𝑑\to 𝐶𝑎𝑡$ to the operad of spliced arrows functor, building the “contour category” of an operad. Using this, we generalize the C-S representation theorem, proving that any context-free language of arrows over a category $𝐶$ is the functorial image of the intersection of a $𝐶$-chromatic tree contour language and a regular language.

The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.

Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and context effects in linear logic, we study logical aspects of this ‘positive’ (covariant) representation, as well as of an associated ‘negative’ (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day’s embedding theorem for monoidal closed categories. Then, we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare logic and linear sequent calculus.

We provide a categorical framework for models of a type theory that has special types for physical quantities. The types are indexed by the physical dimensions that they involve. Fibrations are used to organize this index structure in the models of the type theory. We develop some informative models of this type theory: firstly, a model based on group actions, which captures invariance under scaling, and secondly, a way of constructing new models using relational parametricity.