Abstracts
| Mar. 2023 | March 27, 2023 It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arbitrary algebra. For instance, if M is the free monoid on a set A, then the scalar multiplication function A × M → M is injective. Therefore, when reasoning in the formal theory of monoids under A, it is possible to use this injectivity law to make sound deductions even about monoids under A for which scalar multiplication is not injective — a principle known in algebra as the permanence of identity. Properties of this kind are of fundamental practical importance to the logicians and computer scientists who design and implement computerized proof assistants like Lean and Coq, as they enable the formal reductions of equational problems that make type checking tractable. As type theories have become increasingly more sophisticated, it has become more and more difficult to establish the useful properties of their free models that facilitate effective implementation. These obstructions have facilitated a fruitful return to foundational work in type theory, which has taken on a more geometrical flavor than ever before. Here we expose a modern way to prove a highly non-trivial injectivity law for free models of Martin-Löf type theory, paying special attention to the ways that contemporary methods in type theory have been influenced by three important ideas of the Grothendieck school: the relative point of view, the language of universes, and the recollement of generalized spaces. |
| MSCS | Mathematical Structures in Computer Science March 10, 2023 BibTeX citation@unpublished{sterling:2023:generic,
doi = {10.48550/ARXIV.2210.04202},
author = {Sterling, Jonathan},
title = {What should a generic object be?},
year = {2023},
note = {To appear, Mathematical Structures in Computer Science},
}
Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations, 𝜆2-fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration. |
| MFPS '22 | Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion 38th International Conference on Mathematical Foundations of Programming Semantics February 22, 2023 BibTeX citation@inproceedings{palombi-sterling:2023,
author = {Palombi, Daniele and Sterling, Jonathan},
booktitle = {Proceedings 38th Conference on Mathematical Foundations of Programming Semantics, {MFPS} 2022},
year = {2023},
month = feb,
title = {Classifying topoi in synthetic guarded domain theory},
doi = {10.46298/entics.10323},
}
Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abstracts the concept of guarded recursion frequently employed in the semantics of programming languages. In order to unify the accounts of guarded recursion and coinduction, several authors have enriched SGDT with multiple "clocks" parameterizing different time-streams, leading to more complex and difficult to understand topos models. Until now these topoi have been understood very concretely qua categories of presheaves, and the logico-geometrical question of what theories these topoi classify has remained open. We show that several important topos models of SGDT classify very simple geometric theories, and that the passage to various forms of multi-clock guarded recursion can be rephrased more compositionally in terms of the lower bagtopos construction of Vickers and variations thereon due to Johnstone. We contribute to the consolidation of SGDT by isolating the universal property of multi-clock guarded recursion as a modular construction that applies to any topos model of single-clock guarded recursion. |
| FICS '23 | Fixed Points in Computer Science 2023 February 17, 2023 We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types, based on a combination of guarded recursion and impredicative polymorphism; because our model is based on recursively defined semantic worlds, it is compatible with polymorphism and relational reasoning about stateful abstract datatypes. What is new in relation to prior typed denotational models of higher-order store is that our Kripke worlds need not be syntactically definable, and are thus compatible with relational reasoning in the heap. Our work combines recent advances in the operational semantics of state with the purely denotational viewpoint of synthetic guarded domain theory. |
| Feb. 2023 | Cambridge Computer Laboratory, University of Cambridge February 9, 2023 The great semanticist John Reynolds famously wrote in 1983 that “type structure is a syntactic discipline for enforcing levels of abstraction”. If the last twenty years of programming language semantics and verification have taught us anything, it is that we also need a syntactic discipline for breaking abstraction — in other words, a way to glue together programs and verifications that cut across abstraction barriers. In programming language semantics and verification, the problem of combining multiple levels of abstraction arises when choosing a “level of detail” at which to view program execution: for instance, one could look at program execution as a detailed operational process of discrete steps evincing the cost or complexity of an algorithm, or one could think of it more abstractly as a black box that only sends inputs to outputs. The difficulty is that in practice, verifications tend to cut across this barrier between complexity and functional correctness: for instance, complexity bounds often depend on the functional correctness of subroutines, and the existence of such a bound implies termination (a correctness property). For this reason, it is crucial to develop integrated logical foundations for soundly reasoning using multiple models of execution at the same time, even when they expose different facets of a program's meaning. For the past three years, my research program has been to uncover and exploit the basic “laws of motion” governing all such abstraction barriers, which has led to the solution of a few significant open problems in homotopy type theory and modal type theory, as well as some preliminary applications to security and cost analysis. |
| Dec. 2022 | Workshop on Dependent Type Theory (to celebrate the Defense of Loïc Pujet) December 14, 2022 We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it. |
| Nov. 2022 | Programming, Logic and Semantics, ITU Copenhagen November 8, 2022 Impredicative guarded dependent type theory (iGDTT) is a new version of type theory that combines
guarded recursion (the "later" modality) with impredicative polymorphism (universal and existential types).
It turns out that these two features are sufficient to define a very simple denotational semantics for
System F with recursive types and higher-order store. We believe that the expressivity of iGDTT
brings us one step closer to a general metalanguage for realistic denotational semantics,
and provides a compelling strategy to elude the burden of operational semantics.
As a further benefit, we are now able to justify the extension of full dependent
type theory with a Haskell-style |
| Oct. 2022 | Under review October 10, 2022 BibTeX citation@unpublished{gratzer-sterling-angiuli-coquand-birkedal:2022,
doi = {10.48550/ARXIV.2210.05420},
author = {Gratzer, Daniel and Sterling, Jonathan and Angiuli, Carlo and Coquand, Thierry and Birkedal, Lars},
title = {Controlling unfolding in type theory},
year = {2022},
note = {Unpublished manuscript}
}
We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it. |
| Oct. 2022 | Under review October 6, 2022 BibTeX citation@unpublished{sterling-gratzer-birkedal:2022,
author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars},
year = {2022},
month = jul,
note = {Unpublished manuscript},
title = {Denotational semantics of general store and polymorphism},
}
We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types, based on a combination of guarded recursion and impredicative polymorphism; because our model is based on recursively defined semantic worlds, it is compatible with polymorphism and relational reasoning about stateful abstract datatypes. We then extend our language with modal constructs for proof-relevant relational reasoning based on the logical relations as types principle, in which equivalences between imperative abstract datatypes can be established synthetically. Finally we develop a decomposition of the store model as a general construction that extends an arbitrary polymorphic call-by-push-value adjunction with higher-order store, improving on Levy's possible worlds model construction; what is new in relation to prior typed denotational models of higher-order store is that our Kripke worlds need not be syntactically definable, and are thus compatible with relational reasoning in the heap. Our work combines recent advances in the operational semantics of state with the purely denotational viewpoint of synthetic guarded domain theory. |
| Oct. 2022 | October 1, 2022 BibTeX citation@article{sterling:2022:existentials,
doi = {10.48550/ARXIV.2210.00758},
author = {Sterling, Jonathan},
title = {Reflections on existential types},
publisher = {arXiv},
year = {2022},
note = {Unpublished manuscript},
}
Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple account of first class modules as a mode of use of traditional second class modules in connection with the modal operator induced by a reflective subuniverse, leading to a semantic justification for the rules of first-class modules in languages like OCaml and MoscowML. Additionally, we expose several constructions that give rise to semantic models of ML-style programming languages with both first-class modules and realistic computational effects, culminating in a model that accommodates higher-order first class recursive modules and higher-order store. |
| HoTTEST | Colloquium, HoTTEST Summer School 2022 August 22, 2022 There is a considerable distance between the formal rules of type theory and the code that you must write in order to animate them as a running program. In this colloquium, you will learn the basic techniques of type theoretic implementation in the OCaml programming language, including the representation of syntax as well as type-directed conversion. |
| FSCD '22 | International Conference on Formal Structures for Computation and Deduction (FSCD) June 28, 2022 BibTeX citation@inproceedings{sterling-harper:2022,
author = {Sterling, Jonathan and Harper, Robert},
editor = {Felty, Amy P.},
address = {Dagstuhl, Germany},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
year = {2022},
month = aug,
doi = {10.4230/LIPIcs.FSCD.2022.5},
eprint = {2204.09421},
eprintclass = {cs.PL},
eprinttype = {arXiv},
isbn = {978-3-95977-233-4},
issn = {1868-8969},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Sheaf semantics of termination-insensitive noninterference},
volume = {228},
}
We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper's recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics vis-à-vis an extension of Abadi et al.'s dependency core calculus with a construct for declassifying termination channels. |
| Jun. 2022 | Proofs, Programs and Systems seminar (IRIF PPS) June 9, 2022 Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos' book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists. |
| Jun. 2022 | BibTeX citation@unpublished{sterling:2022:naive,
author = {Sterling, Jonathan},
year = {2022},
month = jun,
note = {Unpublished manuscript},
title = {Na\"{i}ve logical relations in synthetic {Tait} computability},
}
Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos' book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists. |
| WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 20, 2022 BibTeX citation@misc{sterling:2022:wg6,
author = {Sterling, Jonathan},
year = {2022},
month = may,
note = {WG6 kick-off meeting: Syntax and Semantics of Type Theories (Invited Talk)},
title = {Na\"{i}ve logical relations in synthetic {Tait} computability},
}
Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with non-syntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos' book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to non-specialists. |
| Apr. 2022 | Boston University POPV Seminar April 26, 2022 Security-typed programming languages aim to control the flow of high-security information to low security clients. Starting with Abadi et al.'s dependency core calculus, the denotational semantics of such languages has been dominated by an extrinsic approach in which an existing insecure model of computation (e.g. ordinary domains) is restricted by a logical relation of "indistinguishability" to prevent low-security outputs from depending on high-security inputs (noninterference). Thus in the extrinsic approach, security properties are bolted onto an insecure model by brute force, as it were. A more refined information flow policy called termination-insensitive noninterference allows high-security bits to be leaked through termination channels but not through return values; unfortunately, the adaptation of the extrinsic/relational semantics to this more relaxed policy is incompatible with the transitivity of the logical relation, contradicting the intuition of "indistinguishability". In contrast, an intrinsic semantics of security typing would involve a new computational model that evinces secure information flow and noninterference properties directly without any post hoc restriction by a logical relation. We contribute the first such intrinsic semantics of security typing in this sense by considering sheaves of dcpos on a space of abstract behaviors on which security classes arise as open/closed partitions; the security monads then arise as the closed modalities of topos theory that restrict a sheaf to its component over a closed subspace. An advantage of our intrinsic semantics is that termination-insensitive noninterference arises automatically from our computational model, namely the fact that the Sierpiński domain is not a constant sheaf; a further advantage is that our semantics is an instance of standard domain theoretic denotational semantics, albeit over a richer category of domains. Preprint: Sheaf semantics of termination-insensitive noninterference (j.w.w. R. Harper) |
| Feb. 2022 | Under review February 21, 2022 BibTeX citation@unpublished{gratzer-shulman-sterling:2022:universes,
author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
year = {2022},
month = feb,
doi = {10.48550/arXiv.2202.12012},
eprint = {2202.12012},
eprintclass = {math.CT},
eprinttype = {arXiv},
note = {Unpublished manuscript},
title = {Strict universes for Grothendieck topoi},
}
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-Löf type theory. We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-Löf type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi. |
| Feb. 2022 | February 17, 2022 BibTeX citation@unpublished{sterling:2022:bilimits,
author = {Sterling, Jonathan},
year = {2022},
month = feb,
doi = {10.48550/arXiv.2202.08657},
eprint = {2202.08657},
eprintclass = {cs.LO},
eprinttype = {arXiv},
title = {Bilimits in categories of partial maps},
}
The closure of chains of embedding-projection pairs (ep-pairs) under bilimits in some categories of predomains and domains is standard and well-known. For instance, Scott's D∞ construction is well-known to produce directed bilimits of ep-pairs in the category of directed-complete partial orders, and de Jong and Escardó have formalized this result in the constructive domain theory of a topos. The explicit construction of bilimits for categories of predomains and partial maps is considerably murkier as far as constructivity is concerned; most expositions employ the constructive taboo that every lift-algebra is free, reducing the problem to the construction of bilimits in a category of pointed domains and strict maps. An explicit construction of the bilimit is proposed in the dissertation of Claire Jones, but no proof is given so it remained unclear if the category of dcpos and partial maps was closed under directed bilimits of ep-pairs in a topos. We provide a (Grothendieck)-topos-valid proof that the category of dcpos and partial maps between them is closed under bilimits; then we describe some applications toward models of axiomatic and synthetic domain theory. |
| Feb. 2022 | February 15, 2022 BibTeX citation@unpublished{gratzer-shulman-sterling:2022:plump,
author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
year = {2022},
doi = {10.48550/arXiv.2202.07329},
eprint = {2202.07329},
eprintclass = {cs.LO},
eprinttype = {arXiv},
title = {The directed plump ordering},
}
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-Löf type theory. This ordering is similar to the plump ordering but comes equipped with non-empty finite joins in additional to the usual properties of the plump ordering. |
| LMCS | Logical Methods in Computer Science February 9, 2022 BibTeX citation@article{sterling-angiuli-gratzer:2022,
author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
year = {2022},
month = mar,
doi = {10.46298/lmcs-18(1:43)2022},
eprint = {2003.01491},
eprintclass = {cs.LO},
eprinttype = {arXiv},
issue = {1},
journal = {Logical Methods in Computer Science},
title = {{A Cubical Language for Bishop Sets}},
volume = {18},
}
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. |
| WITS '22 | Workshop on the Implementation of Type Systems (keynote) January 22, 2022 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 January 2022 BibTeX citation@article{niu-sterling-grodin-harper:2022,
author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert},
address = {New York, NY, USA},
publisher = {Association for Computing Machinery},
year = {2022},
month = jan,
doi = {10.1145/3498670},
eprint = {2107.04663},
eprintclass = {cs.PL},
eprinttype = {arXiv},
journal = {Proceedings of the ACM on Programming Languages},
number = {POPL},
title = {A Cost-Aware Logical Framework},
volume = {6},
}
We present calf, a cost-aware logical framework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of phase distinctions, we argue that the cost structure of programs motivates a phase distinction between intension and extension. Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, calf presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants. We evaluate calf as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the method of recurrence relations and physicist's method for amortized analysis. We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid's algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and parallel complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in calf by means of a model construction. |
| Nov. 2021 | Computer Laboratory, University of Cambridge November 19, 2021 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 — a new system of axioms that transforms these explicit computations into synthetic manipulations; classical Kripke logical relations can be seen as models or “coordinate systems” for the new geometry of syntax that is beginning to unfold. 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. 2021 | Logic and Semantics Seminar, Aarhus University November 1, 2021 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. 2021 | Doctoral Dissertation, Carnegie Mellon University September 13, 2021 BibTeX citation@phdthesis{sterling:2021:thesis,
author = {Sterling, Jonathan},
school = {Carnegie Mellon University},
year = {2021},
doi = {10.5281/zenodo.6990769},
note = {Version 1.1, revised May 2022},
number = {CMU-CS-21-142},
title = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory},
}
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. 2021 | CMU Speakers Club August 24, 2021 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 July 7, 2021 BibTeX citation@inproceedings{sterling-angiuli:2021,
author = {Sterling, Jonathan and Angiuli, Carlo},
address = {Los Alamitos, CA, USA},
publisher = {IEEE Computer Society},
booktitle = {2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
year = {2021},
month = jul,
doi = {10.1109/LICS52264.2021.9470719},
eprint = {2101.11479},
eprintclass = {cs.LO},
eprinttype = {arXiv},
pages = {1--15},
title = {Normalization for Cubical Type Theory},
}
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 May 19, 2021 BibTeX citation@article{sterling:2021:bhfs,
author = {Sterling, Jonathan},
publisher = {Cambridge University Press},
date = {2021},
doi = {10.1017/S0956796821000095},
eprint = {1608.03814},
eprintclass = {math.LO},
eprinttype = {arXiv},
journaltitle = {Journal of Functional Programming},
note = {\emph{Bob Harper Festschrift Collection}},
pages = {e11},
title = {Higher order functions and Brouwer's thesis},
volume = {31},
}
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. |
| JACM | Journal of the ACM May 2021 BibTeX citation@article{sterling-harper:2021,
author = {Sterling, Jonathan and Harper, Robert},
address = {New York, NY, USA},
publisher = {Association for Computing Machinery},
year = {2021},
month = oct,
doi = {10.1145/3474834},
eprint = {2010.08599},
eprintclass = {cs.PL},
eprinttype = {arXiv},
issn = {0004-5411},
journal = {Journal of the ACM},
number = {6},
title = {Logical Relations as Types: Proof-Relevant Parametricity for Program Modules},
volume = {68},
}
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. |
| May 2021 | 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 |
| Apr. 2021 | CCS Colloquium, Augusta University This is joint work with Robert Harper. 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. 2021 | Pittsburgh's HoTT 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 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 : 𝕀. (j.w.w. C. Angiuli) |
| ML '21 | BibTeX citation@unpublished{sterling-harper:2021:mlw,
author = {Sterling, Jonathan and Harper, Robert},
url = {https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/5/A-metalanguage-for-multi-phase-modularity},
year = {2021},
month = aug,
note = {ML 2021 abstract and talk},
title = {A metalanguage for multi-phase modularity},
}
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 φML for multi-phase modularity in which these concepts are treated individually, supporting the definition of high-level modular constructs such as generative and applicative functors, as well as all extant forms of structure sharing. |
| Dec. 2020 | BibTeX citation@unpublished{gratzer-sterling:2020,
author = {Gratzer, Daniel and Sterling, Jonathan},
year = {2020},
eprint = {2012.10783},
eprintclass = {cs.LO},
eprinttype = {arXiv},
title = {Syntactic categories for dependent type theory: sketching and adequacy},
}
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. |
| Jun. 2020 | 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. |
| HoTTEST | Homotopy Type Theory Electronic Seminar Talks March 2020 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. |
| Jan. 2020 | 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. |
| 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 BibTeX citation@article{gratzer-sterling-birkedal:2019,
author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
location = {New York, NY, USA},
publisher = {ACM},
date = {2019-07},
doi = {10.1145/3341711},
issn = {2475-1421},
journaltitle = {Proceedings of the ACM on Programming Languages},
keywords = {Modal types,dependent types,normalization by evaluation,type-checking},
number = {ICFP},
pages = {107:1--107:29},
title = {Implementing a Modal Dependent Type Theory},
volume = {3},
}
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. |
| FSCD '19 | International Conference on Formal Structures for Computation and Deduction (FSCD) FSCD '19 Best Paper Award for Junior Researchers BibTeX citation@inproceedings{sterling-angiuli-gratzer:2019,
author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
editor = {Geuvers, Herman},
location = {Dagstuhl, Germany},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
url = {http://drops.dagstuhl.de/opus/volltexte/2019/10538},
booktitle = {Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
date = {2019},
doi = {10.4230/LIPIcs.FSCD.2019.31},
eprint = {1904.08562},
eprinttype = {arXiv},
isbn = {978-3-95977-107-8},
issn = {1868-8969},
pages = {31:1--31:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Cubical Syntax for Reflection-Free Extensional Equality},
volume = {131},
}
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. |
| LICS '18 | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) BibTeX citation@inproceedings{sterling-harper:2018,
author = {Sterling, Jonathan and Harper, Robert},
title = {Guarded Computational Type Theory},
booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
series = {LICS '18},
year = {2018},
isbn = {978-1-4503-5583-4},
location = {Oxford, United Kingdom},
pages = {879--888},
numpages = {10},
url = {http://doi.acm.org/10.1145/3209108.3209153},
doi = {10.1145/3209108.3209153},
acmid = {3209153},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {clocks, dependent types, guarded recursion, operational semantics, type theory},
}
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 BibTeX citation@inproceedings{redprl:2018:lfmtp,
author = {Angiuli, Carlo and Cavallo, Evan and {Hou (Favonia)}, Kuen-Bang and Harper, Robert and Sterling, Jonathan},
editor = {Blanqui, Fr\'{e}d\'{e}ric and Reis, Giselle},
publisher = {Open Publishing Association},
booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018.},
date = {2018},
doi = {10.4204/EPTCS.274.1},
pages = {1--10},
title = {{The \textsf{\textcolor[rgb]{.91,.31,.27}{Red}PRL} Proof Assistant (Invited Paper)}},
}
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. BibTeX citation@inbook{valentine-sterling:2016,
author={Valentine, Rebecca and Sterling, Jonathan},
editor={Redmond, Juan and Pombo Martins, Olga and Nepomuceno Fern{\'a}ndez, {\'A}ngel},
title={Dependent Types for Pragmatics},
booktitle={Epistemology, Knowledge and the Impact of Interaction},
year={2016},
publisher={Springer International Publishing},
address={Cham},
pages={123--139},
isbn={978-3-319-26506-3},
doi={10.1007/978-3-319-26506-3_4},
}
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. |