WITS '22 | Workshop on the Implementation of Type Systems (keynote) For six years, I have served as the founder and technical leader of the RedPRL Development Team which has produced three interactive proof assistants for variants of cubical type theory: RedPRL, redtt, and cooltt. I will share several lessons that we have learned about the design and implementation of homotopical proof assistants along this journey. This talk discusses joint work with C. Angiuli, E. Cavallo, Favonia, R. Harper, and R. Mullanix. |

POPL '22 | 49th ACM SIGPLAN Symposium on Principles of Programming Languages We present As a full-spectrum dependent type theory, |

Dec. '21 | The closure of chains of embedding-projection pairs ( |

Nov. 19, '21 | Computer Laboratory, University of Cambridge The purpose of this talk is to pose the question, “What are the Euclid’s postulates for syntactic metatheory?” In the fourth century B.C.E., the Greek mathematician Euclid set down his famous postulates for plane geometry, explaining geometric shapes in terms of rules that govern their construction and incidence. The dialectical relationship between theories (axioms) and their models (coordinate systems) has been the driving force in the last two millennia of geometrical investigation. In logic and computer science, workers in the “syntactic metatheory” investigate questions that lie on the fringe between a theory and its models — definability, normalization, decidability, conservativity, computational adequacy, parametricity, type safety, etc. Dominant methods attack these questions by means of explicit computations (e.g. Kripke logical relations) which practitioners have found to be both reliable and somewhat opaque. In this talk, I introduce Synthetic Tait computability has already been employed to positively resolve the normalization and decidability conjectures for cubical type theory, as well as a number of other recent results. |

Nov. 1, '21 | Logic and Semantics Seminar, Aarhus University The fundamental contradiction of programming and program verification can be located in the tension between abstraction and composition. We make programs more abstract in order to prevent bad interactions between components; on the other side of the coin, we impede the composition of components when we abstract them. Modern programming practice evinces many distinct levels of abstraction that must be considered at the same time — for instance, compilers break module boundaries during linking, complexity analysis breaks the abstraction of extensional equivalence, and logical relations proofs break the abstraction of closure under substitution. What is needed to meet this challenge is linguistic tools that smoothly interpolate between these different levels of abstraction. Building on my doctoral dissertation and joint work with Bob Harper, I introduce a new plan for modal programming languages and logics that treat the transition between different abstraction levels as a first-class notion. |

Sep. 13, '21 | Doctoral Dissertation, Carnegie Mellon University 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. |

Aug. 24, '21 | CMU Speakers Club Programmers use abstraction to hide representation details from ourselves: either to avoid mistakes (e.g. confusing a list index with a length) or to exploit representation invariants (e.g. two implementations of the QUEUE interface are indistinguishable). These abstraction boundaries can unfortunately impede the linking of smaller program units into efficient composite programs, because compilers must exploit representation details in order to produce efficient code. Sometimes seen as the "waterloo of separate compilation", the need to break abstraction is answered by whole-program analysis techniques that break all abstractions (as in the MLton compiler for Standard ML). Separate compilation, however, has a number of advantages including speed, parallelization, and elegance. We present an alternative type theoretic account of abstraction-breaking during compilation based on the famous phase distinction of ML languages; rather than distinguishing between compiletime and runtime, we focus on separating "devtime" from compiletime. Our framework allows the programmer to selectively reveal representation details to the compiler without giving up the representation independence properties guaranteed by "devtime" type correctness. We also describe an application to the problem of printf-debugging, which is ordinarily obstructed by abstraction. |

LICS '21 | 36th Annual Symposium on Logic in Computer Science We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors. |

JFP | Journal of Functional Programming, Bob Harper Festschrift Collection Extending Martín Escardó's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a functional of type (ℕ→ℕ)→ℕ in Gödel's System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type ℕ→ℕ, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer's famous "mental constructions" of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order. |

May '21 | Padova Logic Seminar We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. The main difficulty in comparison to conventional type theory is located in a new feature of cubical type theories, the absence of a stable notion of neutral term: for instance, the path application |

JACM | Journal of the ACM The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh "synthetic" take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects. Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs -- simplifying the metatheory of strong sums over the collection of types, for although there can be no "relation classifying relations", one easily accommodates a "family classifying small families". Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan "logical relations as types", iterating our modal account of the phase distinction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant. |

Apr. '21 | CCS Colloquium, Augusta University
How do you prove that two implementations of an abstract type behave the same in all configurations? Reynolds famously employed logical relations to establish such results; roughly, a logical relation is a structure-respecting relation between two interpretations of a theory that evinces, in the base case, a desirable invariant. We present a synthetic way to understand and interact with logical relations, related to classical logical relations in the same way that Euclidean geometry relates to point-sets. Previously a logical relation was defined in terms of the (complicated) details of how it is constructed as a certain kind of relation over syntax. We instead take the simpler view that everything in sight is a logical relation, and then use modalities to isolate those logical relations that are degenerate in either the syntactic or the semantic direction. Our “logical relations as types” principle has led to a new account of modules and representation independence (S., Harper), as well as the first proofs of normalization for cubical type theory (S., Angiuli) and general multi-modal dependent type theory (Gratzer). |

Feb. '21 | Pittsburgh's HoTT Seminar (J.w.w. Carlo Angiuli) We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. The main difficulty in comparison to conventional type theory is located in a new feature of cubical type theories, the absence of a stable notion of neutral term: for instance, the path application p(i) ceases to be neutral within its “locus of instability” ∂(i) and must compute to an endpoint. We introduce a new, geometrically-inspired generalization of the notion of neutral term, stabilizing neutrals by gluing them together with partial computability data along their loci of instability — when the locus of instability is nowhere, a stabilized neutral is a conventional neutral, and when the locus of instability is everywhere, a stabilized neutral is just computability data. Our normalization result is based on a reduction-free Artin gluing argument, and yields an injective function from equivalence classes of terms in context to a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality, as well as injectivity of type constructors in contexts formed by assuming variables x : A and dimensions i : 𝕀. |

ML '21 | Type abstraction, the phase distinction, and computational effects all play an important role in the design and implementation of ML-style module systems. We propose a simple type theoretic metalanguage |

Dec. '20 | We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one may define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework, following the "judgments as types" principle. The concentration of type theories into their locally Cartesian closed categories of judgments is particularly convenient for proving syntactic metatheorems by semantic means (canonicity, normalization, etc.). Perhaps surprisingly, the notion of a context plays no role in the definitions of type theories in this sense, but the structure of a class of display maps can be imposed on a theory post facto wherever needed, as advocated by the Edinburgh school and realized by the Uemura has proposed representable map categories together with a stratified logical framework for similar purposes. The stratification in Uemura's framework restricts the use of dependent products to be strictly positive, in contrast to the tradition of Martin-Löf's logical framework and Schroeder-Heister's analysis of higher-level deductions. We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories. |

Aug. '20 | Doctoral Thesis Proposal, Carnegie Mellon University 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 property of their initial models to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory enable the design and implementation of correct-by-construction elaboration algorithms, providing a principled interface between real proof assistants and ideal mathematics. |

Jun. '20 | Every Proof Assistant redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring computational versions of function extensionality, higher inductive types, and univalence. Building on ideas from Epigram, Agda, and Idris, redtt introduces a new cubical take on interactive proof development with holes. We will first introduce the basics of cubical type theory and then dive into an interactive demonstration of redtt’s features and its mathematical library. After this we will catch a first public glimpse of the future of redtt, a new prototype that our team is building currently code-named "cooltt": cooltt introduces syntax to split on disjunctions of cofibrations in arbitrary positions, implementing the full definitional eta law for disjunction. While cooltt is still in the early stages, it already has full support for univalence and cubical interactive proof development. |

Mar. '20 | Homotopy Type Theory Electronic Seminar Talks What type theorists and other researchers in type theory have in common is that they study theorems that hold of the initial model of type theory; but type theorists especially emphasize the theorems whose statements are sufficiently non-type-theoretic that they need not be preserved by homomorphisms of models. These theorems, sometimes called "metatheorems" or "admissibilities", are the means by which we conceive and justify computerized implementations of type theory, including canonicity, normalization, and decidability of type checking and judgmental equality. The main tool for proving such theorems is Tait's method of computability, which has in the past several years been subject to a rapid campaign of rectification using the categorical language of Artin gluing. I will give an overview of this brave new "objective computability", emphasizing my recent joint work with Angiuli and Gratzer on a general gluing theorem for models of MLTT along flat functors into Grothendieck topoi, with an application to cubical type theory. |

Feb. '20 | We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) by Artin gluing. |

Jan. '20 | CMU HoTT Seminar We extend the theory of Artin gluing to strict dependent type theory: given a flat functor F : C → E from the category of contexts a model of Martin-Löf type theory into a Grothendieck topos E, we may construct the F-computability families model of type theory. Our theorem extends to MLTT with a (strict, weak) universe à la Tarski if E may be equipped with a (strict, weak) universe à la Tarski. We introduce a more tractable approach to gluing models of type theory, working primarily within a suitably enlarged category of computability families which are not all tracked by syntactical entities, but which is densely generated by the subcategory of such computability families. |

FSCD '19 | International Conference on Formal Structures for Computation and Deduction (FSCD), 2019 FSCD '19 Best Paper Award for Junior Researchers We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false. |

HoTT '19 | International Conference on Homotopy Type Theory, 2019 We contribute XTT, a cubical reconstruction of Observational Type Theory which extends intensional type theory with a dependent equality type that enjoys function extensionality and judgmental unicity of identity proofs. XTT employs a variant of the Cartesian cubical Kan operations satisfying regularity (i.e., transport in constant type families is judgmentally constant), allowing its equality type to model Martin-Lof’s identity type judgmentally. We prove canonicity for the initial model of XTT (i.e., any closed term of boolean type is equal to either true or false) using a novel cubical extension (independently proposed by Awodey) of the categorical gluing technique inspired by Coquand and Shulman, in which we glue the fundamental fibration of a category of augmented Cartesian cubical sets along a cubical nerve. We conjecture that our methods will extend to open terms, allowing us to establish normalization and decidability of the typing relation. |

ICFP '19 | International Conference on Functional Programming (ICFP), 2019 ICFP '19 Distinguished Paper Award Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theory MLTT🔒 supporting the connectives of standard Martin-Löf Type Theory as well as an S4-style necessity operator. MLTT🔒 supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type checking algorithm for MLTT🔒, using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant for MLTT🔒, demonstrating the ease of applying our techniques. |

LICS '18 | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes. We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics. |

LFMTP '18 | International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths. |

LEUS | In: Redmond J., Pombo Martins O., Nepomuceno Fernández Á. (eds) Epistemology, Knowledge and the Impact of Interaction. Logic, Epistemology, and the Unity of Science, vol 38. Springer, Cham. In this paper, we present an extension to Martin-Löf’s Intuitionistic Type Theory which gives natural solutions to problems in pragmatics, such as pronominal reference and presupposition. Our approach also gives a simple account of donkey anaphora without resorting to exotic scope extension of the sort used in Discourse Representation Theory and Dynamic Semantics, thanks to the proof-relevant nature of type theory. |