Abstracts

 Oct. 2022 Coming soonPreprint Reflections on existential typesJ. SterlingabstractExistential types are reconstructed in terms of reflective subuniverses and dependent sums. The folklore decomposition detailed here leads to a particularly simple account of first class modules as a mode of use of traditional second class modules, giving a new perspective on the classic problem of supporting a "dot notation" for the components of abstract types. Sep. 2022 Preprint Denotational semantics of general store and polymorphismSeptember 9, 2022BibTeX 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. HoTTEST Invited How to code your own type theoryColloquium, HoTTEST Summer School 2022August 22, 2022There 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. Jul. 2022 Preprint What should a generic object be?J. SterlingUnder reviewJuly 13, 2022BibTeX citation@unpublished{sterling:2022:generic, author = {Sterling, Jonathan}, year = {2022}, month = jul, note = {Unpublished manuscript}, title = {What should a generic object be?}, } Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of generic object and split generic object, 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. given by Jacobs are strict enough to rule out many fundamental examples that must be accounted for by any candidate definition; for instance, realizability almost never gives rise to a tripos in the sense of Jacobs. We argue for a new alignment of terminology that emphasizes the forms of generic object that appear most commonly in nature, i.e. in the study of internal categories, triposes, topoi, and the denotational semantics of polymorphic types. In addition, we propose a new class of acyclic generic objects inspired by recent developments in the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibered category. FSCD '22 Sheaf semantics of termination-insensitive noninterferenceInternational Conference on Formal Structures for Computation and Deduction (FSCD)June 28, 2022BibTeX 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 Invited Naïve logical relations in synthetic Tait computabilityProofs, Programs and Systems seminar (IRIF PPS)June 9, 2022Logical 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 Preprint Naïve logical relations in synthetic Tait computabilityJ. SterlingBibTeX 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 Invited Naïve logical relations in synthetic Tait computabilityWG6 kick-off meeting: Syntax and Semantics of Type TheoriesMay 20, 2022BibTeX 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 Invited Intrinsic semantics of termination-insensitive noninterferenceBoston University POPV SeminarApril 26, 2022Security-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. (j.w.w. R. Harper) MFPS '22 To appear Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion38th International Conference on Mathematical Foundations of Programming SemanticsApril 19, 2022BibTeX citation@inproceedings{palombi-sterling:2022, author = {Palombi, Daniele and Sterling, Jonathan}, url = {https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf}, booktitle = {Proceedings 38th Conference on Mathematical Foundations of Programming Semantics, {MFPS} 2022}, year = {2022}, note = {To appear}, title = {Classifying topoi in synthetic guarded domain theory}, } 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. Feb. 2022 Preprint Strict universes for Grothendieck topoiUnder reviewFebruary 21, 2022BibTeX 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 Notes Bilimits in categories of partial mapsJ. SterlingFebruary 17, 2022BibTeX 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 Notes The directed plump orderingFebruary 15, 2022BibTeX 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 A Cubical Language for Bishop SetsLogical Methods in Computer ScienceFebruary 9, 2022BibTeX 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 Invited Make Three To Throw Away: Frontiers in Homotopical Proof AssistantsWorkshop on the Implementation of Type Systems (keynote)January 22, 2022For 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 A cost-aware logical framework49th ACM SIGPLAN Symposium on Principles of Programming LanguagesJanuary 2022BibTeX 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 Invited Towards a geometry for syntaxComputer Laboratory, University of CambridgeNovember 19, 2021The 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 Between abstraction and composition...Logic and Semantics Seminar, Aarhus UniversityNovember 1, 2021The 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 First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type TheoryDoctoral Dissertation, Carnegie Mellon UniversitySeptember 13, 2021BibTeX 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 Abstraction, composition, and the phase distinctionCMU Speakers ClubAugust 24, 2021Programmers 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 Normalization for Cubical Type theory36th Annual Symposium on Logic in Computer ScienceJuly 7, 2021BibTeX 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 Higher order functions and Brouwer's ThesisJ. SterlingJournal of Functional Programming, Bob Harper Festschrift CollectionMay 19, 2021BibTeX 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 Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACMMay 2021BibTeX 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 Invited Normalization for Cubical Type TheoryPadova Logic SeminarWe 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 : 𝕀. Apr. 2021 Invited Logical Relations As TypesCCS Colloquium, Augusta UniversityThis 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 Normalization for Cubical Type theoryPittsburgh's HoTT SeminarWe 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 A metalanguage for multi-phase modularityML Family Workshop 2021BibTeX 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 Notes Syntactic categories for dependent type theory: sketching and adequacyBibTeX 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 %worlds declarations of the Twelf proof assistant. 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 Invited redtt and the future of Cartesian cubical type theoryEvery Proof Assistantredtt 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. 2020 Invited Objective Metatheory of Dependent Type TheoriesHomotopy Type Theory Electronic Seminar TalksWhat 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 Gluing Models of Type Theory Along Flat FunctorsCMU HoTT SeminarWe 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 Cubical Exact Equality and Categorical GluingInternational Conference on Homotopy Type Theory, 2019We 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 Implementing a Modal Dependent Type TheoryInternational Conference on Functional Programming (ICFP), 2019ICFP '19 Distinguished Paper AwardBibTeX 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 Cubical Syntax for Reflection-Free Extensional EqualityInternational Conference on Formal Structures for Computation and Deduction (FSCD)FSCD '19 Best Paper Award for Junior ResearchersBibTeX 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 Guarded Computational Type TheoryProceedings 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 Invited The RedPRL Proof AssistantInternational Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018BibTeX 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 Invited Dependent Types for PragmaticsR. Valentine and J. SterlingIn: 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.