13 Search Results for "Licata, Daniel R."

Document
DOI: 10.4230/LIPIcs.CSL.2026.20
On Left Adjoints Preserving Colimits in HoTT

Authors: Perry Hart

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.
Cite as

Perry Hart. On Left Adjoints Preserving Colimits in HoTT. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hart:LIPIcs.CSL.2026.20,
  author =	{Hart, Perry},
  title =	{{On Left Adjoints Preserving Colimits in HoTT}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.20},
  URN =		{urn:nbn:de:0030-drops-254442},
  doi =		{10.4230/LIPIcs.CSL.2026.20},
  annote =	{Keywords: wild categories, colimits, adjunctions, homotopy type theory, category theory, synthetic homotopy theory, higher inductive types, modalities}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.7
A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.
Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.6
Data Types with Symmetries via Action Containers

Authors: Philipp Joram and Niccolò Veltri

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
  author =	{Joram, Philipp and Veltri, Niccol\`{o}},
  title =	{{Data Types with Symmetries via Action Containers}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.6},
  URN =		{urn:nbn:de:0030-drops-233681},
  doi =		{10.4230/LIPIcs.TYPES.2024.6},
  annote =	{Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.9
Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Authors: Robert Rose and Daniel R. Licata

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete.
Cite as

Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rose_et_al:LIPIcs.TYPES.2024.9,
  author =	{Rose, Robert and Licata, Daniel R.},
  title =	{{Complexity of Cubical Cofibration Logics I: coNP-Complete Examples}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9},
  URN =		{urn:nbn:de:0030-drops-233711},
  doi =		{10.4230/LIPIcs.TYPES.2024.9},
  annote =	{Keywords: cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.46
Coslice Colimits in Homotopy Type Theory

Authors: Perry Hart and Kuen-Bang Hou (Favonia)

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between colimits in coslices of a universe, called coslice colimits, and colimits in the universe (i.e., ordinary colimits). To derive this characterization, we find an explicit construction of colimits in coslices that is tailored to reveal the connection. We use the construction to derive properties of colimits. Notably, we prove that the forgetful functor from a coslice creates colimits over trees. We also use the construction to examine how colimits interact with orthogonal factorization systems and with cohomology theories. As a consequence of their interaction with orthogonal factorization systems, all pointed colimits (special kinds of coslice colimits) preserve n-connectedness, which implies that higher groups are closed under colimits on directed graphs. We have formalized our main construction of the coslice colimit functor in Agda.
Cite as

Perry Hart and Kuen-Bang Hou (Favonia). Coslice Colimits in Homotopy Type Theory. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hart_et_al:LIPIcs.CSL.2025.46,
  author =	{Hart, Perry and Hou (Favonia), Kuen-Bang},
  title =	{{Coslice Colimits in Homotopy Type Theory}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{46:1--46:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.46},
  URN =		{urn:nbn:de:0030-drops-228039},
  doi =		{10.4230/LIPIcs.CSL.2025.46},
  annote =	{Keywords: colimits, homotopy type theory, category theory, higher inductive types, synthetic homotopy theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.14
Two-Dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.
Cite as

G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14},
  URN =		{urn:nbn:de:0030-drops-203438},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
  annote =	{Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.6
{mitten}: A Flexible Multimodal Proof Assistant

Authors: Philipp Stassen, Daniel Gratzer, and Lars Birkedal

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.
Cite as

Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6,
  author =	{Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars},
  title =	{{\{mitten\}: A Flexible Multimodal Proof Assistant}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.6},
  URN =		{urn:nbn:de:0030-drops-184498},
  doi =		{10.4230/LIPIcs.TYPES.2022.6},
  annote =	{Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.13
Internal Parametricity for Cubical Type Theory

Authors: Evan Cavallo and Robert Harper

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.
Cite as

Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13,
  author =	{Cavallo, Evan and Harper, Robert},
  title =	{{Internal Parametricity for Cubical Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13},
  URN =		{urn:nbn:de:0030-drops-116564},
  doi =		{10.4230/LIPIcs.CSL.2020.13},
  annote =	{Keywords: parametricity, cubical type theory, higher inductive types}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.14
Unifying Cubical Models of Univalent Type Theory

Authors: Evan Cavallo, Anders Mörtberg, and Andrew W Swan

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.
Cite as

Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.14,
  author =	{Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W},
  title =	{{Unifying Cubical Models of Univalent Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14},
  URN =		{urn:nbn:de:0030-drops-116578},
  doi =		{10.4230/LIPIcs.CSL.2020.14},
  annote =	{Keywords: Cubical Set Models, Cubical Type Theory, Homotopy Type Theory, Univalent Foundations}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.31
Cubical Syntax for Reflection-Free Extensional Equality

Authors: Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
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.
Cite as

Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31,
  author =	{Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  title =	{{Cubical Syntax for Reflection-Free Extensional Equality}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{31:1--31:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31},
  URN =		{urn:nbn:de:0030-drops-105387},
  doi =		{10.4230/LIPIcs.FSCD.2019.31},
  annote =	{Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.22
Internal Universes in Models of Homotopy Type Theory

Authors: Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.
Cite as

Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{licata_et_al:LIPIcs.FSCD.2018.22,
  author =	{Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
  title =	{{Internal Universes in Models of Homotopy Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.22},
  URN =		{urn:nbn:de:0030-drops-91929},
  doi =		{10.4230/LIPIcs.FSCD.2018.22},
  annote =	{Keywords: cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.24
Call-by-Name Gradual Type Theory

Authors: Max S. New and Daniel R. Licata

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism. These dynamism judgements build on prior work in blame calculi and on the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality (eta) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of the interpretation of gradual typing using contracts, and use it to build some concrete domain-theoretic models of gradual typing.
Cite as

Max S. New and Daniel R. Licata. Call-by-Name Gradual Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{new_et_al:LIPIcs.FSCD.2018.24,
  author =	{New, Max S. and Licata, Daniel R.},
  title =	{{Call-by-Name Gradual Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.24},
  URN =		{urn:nbn:de:0030-drops-91944},
  doi =		{10.4230/LIPIcs.FSCD.2018.24},
  annote =	{Keywords: Gradual Typing, Type Systems, Program Logics, Category Theory, Denotational Semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.25
A Fibrational Framework for Substructural and Modal Logics

Authors: Daniel R. Licata, Michael Shulman, and Mitchell Riley

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We define a general framework that abstracts the common features of many intuitionistic substructural and modal logics / type theories. The framework is a sequent calculus / normal-form type theory parametrized by a mode theory, which is used to describe the structure of contexts and the structural properties they obey. In this sequent calculus, the context itself obeys standard structural properties, while a term, drawn from the mode theory, constrains how the context can be used. Product types, implications, and modalities are defined as instances of two general connectives, one positive and one negative, that manipulate these terms. Specific mode theories can express a range of substructural and modal connectives, including non-associative, ordered, linear, affine, relevant, and cartesian products and implications; monoidal and non-monoidal functors, (co)monads and adjunctions; n-linear variables; and bunched implications. We prove cut (and identity) admissibility independently of the mode theory, obtaining it for many different logics at once. Further, we give a general equational theory on derivations / terms that, in addition to the usual beta/eta-rules, characterizes when two derivations differ only by the placement of structural rules. Additionally, we give an equivalent semantic presentation of these ideas, in which a mode theory corresponds to a 2-dimensional cartesian multicategory, the framework corresponds to another such multicategory with a functor to the mode theory, and the logical connectives make this into a bifibration. Finally, we show how the framework can be used both to encode existing existing logics / type theories and to design new ones.
Cite as

Daniel R. Licata, Michael Shulman, and Mitchell Riley. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{licata_et_al:LIPIcs.FSCD.2017.25,
  author =	{Licata, Daniel R. and Shulman, Michael and Riley, Mitchell},
  title =	{{A Fibrational Framework for Substructural and Modal Logics}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.25},
  URN =		{urn:nbn:de:0030-drops-77400},
  doi =		{10.4230/LIPIcs.FSCD.2017.25},
  annote =	{Keywords: type theory, modal logic, substructural logic, homotopy type theory}
}
  • Refine by Type
  • 13 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 1 2024
  • 1 2023
  • 2 2020
  • Show More...

  • Refine by Author
  • 4 Licata, Daniel R.
  • 2 Cavallo, Evan
  • 2 Gratzer, Daniel
  • 2 Hart, Perry
  • 1 Angiuli, Carlo
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs

  • Refine by Classification
  • 10 Theory of computation → Type theory
  • 3 Theory of computation → Categorical semantics
  • 2 Theory of computation → Denotational semantics
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Algebraic semantics
  • Show More...

  • Refine by Keyword
  • 5 homotopy type theory
  • 3 higher inductive types
  • 2 Dependent type theory
  • 2 Homotopy Type Theory
  • 2 category theory
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact