pith. sign in

arxiv: 2507.08759 · v4 · pith:PLUPRAU2new · submitted 2025-07-11 · 💻 cs.PL · cs.LO

Dependent Multiplicities in Dependent Linear Type Theory

Maximilian Dor\'e This is my paper

Pith reviewed 2026-05-22 00:24 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords dependent linear typesmultiplicitiesresource annotationsbranchingrecursionW-typesquantitative typinglinear logic embedding
0
0 comments X

The pith

Multiplicities of variables can depend on other values, allowing precise resource counts for branching and recursive programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs a dependent linear type theory in which the number of times a variable may be used is itself a term that can mention other variables. This produces resource annotations that change according to the path taken in a branch or the depth reached in a recursion, something earlier linear type systems could not express exactly. The construction proceeds by embedding linear logic inside a dependent type theory and fixing the interaction rules so that the host theory’s natural numbers supply the multiplicities. The resulting system also accommodates W-types, thereby giving a uniform resource treatment to a broad class of inductive data structures, and admits a straightforward implementation inside an existing language such as Agda.

Core claim

By embedding linear logic into dependent type theory and specifying the interaction rules, one obtains a quantitative type system whose multiplicities may depend on values; the system remains consistent, supports W-types, and is interpreted as categories with families indexed in symmetric monoidal categories, thereby generalising earlier quantitative models.

What carries the argument

The embedding of linear logic into dependent type theory together with the specified interaction rules that let multiplicities be formed from the natural numbers of the host theory.

If this is right

  • Branching programs receive resource annotations that differ on each branch according to the value that decides the branch.
  • Recursive definitions can be given multiplicity expressions that refer to the recursion parameter or to earlier results.
  • W-types receive a uniform, resource-sensitive typing that covers a large family of inductive structures.
  • Existing dependently typed languages can incorporate the rules without altering their core syntax, as demonstrated by an Agda encoding.
  • The semantics generalise quantitative categories with families by indexing them in symmetric monoidal categories.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same dependent-multiplicity mechanism could be applied to track usage of other linear resources such as channels or memory cells whose availability depends on data.
  • Compilers that already use dependent types might gain automatic resource-bound inference by reusing the existing term language for multiplicities.
  • The approach suggests a route to typing protocols whose message counts or buffer sizes are computed from earlier messages.

Load-bearing premise

The chosen interaction rules between the embedded linear logic and the surrounding dependent type theory produce a consistent system.

What would settle it

A concrete recursive function whose resource usage depends on an input value, together with a derivation that the dependent-multiplicity rules accept but that leads to an inconsistency or a rejected Agda term.

Figures

Figures reproduced from arXiv: 2507.08759 by Maximilian Dor\'e.

Figure 1
Figure 1. Figure 1: Basic rules for supplies and productions. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Productions for data types. We extend our production relation from [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Rules for function types. In [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Rules for the linear exponential. The rules in [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗
read the original abstract

We present a novel dependent linear type theory in which the multiplicity of some variable-i.e., the number of times the variable can be used in a program-can depend on other variables. This allows us to give precise resource annotations to programs involving branching and recursion that cannot be adequately typed in other theories. Our type system is obtained by embedding linear logic into dependent type theory and specifying how the embedded logic interacts with the host theory. We can then use the natural numbers of the dependent type theory to derive a quantitative typing system with dependent multiplicities. Our theory supports W-types, thereby giving a principled resource-aware treatment of a large class of inductive types. We characterise the semantics as Categories with Families indexed in symmetric monoidal categories, thereby generalising Quantitative Categories with Families. Existing dependently typed languages can easily be extended with our system, which we demonstrate with an implementation in Agda.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents a novel dependent linear type theory obtained by embedding linear logic into dependent type theory, with interaction rules that allow multiplicities to be drawn from the host natural numbers and to depend on other variables. This enables precise resource annotations for branching and recursion. The system supports W-types for a resource-aware treatment of inductive types and is semantically characterized as Categories with Families indexed in symmetric monoidal categories, generalizing Quantitative CwFs. Practicality is demonstrated via an Agda implementation.

Significance. If the embedding and interaction rules produce a consistent quantitative system, the work would advance resource-aware dependent typing by handling cases involving branching and recursion that existing theories cannot address. The generalization of Quantitative CwFs and the W-type support are notable strengths. The Agda implementation supplies reproducible examples and shows how existing dependently typed languages can be extended.

major comments (2)
  1. [Semantics characterisation] The manuscript characterises the semantics as CwFs indexed in symmetric monoidal categories (generalising Quantitative CwFs) yet supplies no full metatheoretic argument—such as subject reduction, linearity preservation, or normalisation—for the claim that the indexing and interaction rules prevent resource duplication or ill-defined multiplicities when a multiplicity expression depends on a linear variable or appears under recursion via W-types. This is load-bearing for the central consistency claim.
  2. [Embedding and interaction rules] The embedding construction and interaction rules between the embedded linear logic and the host DTT are outlined in the abstract and introduction, but the paper does not provide detailed proof sketches or derivations showing that these rules yield a consistent quantitative typing system whose multiplicities correctly handle branching and recursion. Without this, the support for the main claim remains incomplete.
minor comments (1)
  1. [Abstract] The abstract could include a forward reference to the section containing the Agda implementation to improve navigation for readers interested in the concrete extension of existing languages.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and positive evaluation of the significance of our work on dependent multiplicities. The comments highlight important points regarding the metatheoretic foundations, which we address below. We have revised the manuscript to include additional clarifications and proof outlines that strengthen the consistency arguments without altering the core contributions.

read point-by-point responses

  1. Referee: [Semantics characterisation] The manuscript characterises the semantics as CwFs indexed in symmetric monoidal categories (generalising Quantitative CwFs) yet supplies no full metatheoretic argument—such as subject reduction, linearity preservation, or normalisation—for the claim that the indexing and interaction rules prevent resource duplication or ill-defined multiplicities when a multiplicity expression depends on a linear variable or appears under recursion via W-types. This is load-bearing for the central consistency claim.

    Authors: We agree that a more explicit metatheoretic development would strengthen the presentation. The semantic model in indexed CwFs is designed so that linearity and resource accounting are preserved by the categorical structure itself: morphisms in the symmetric monoidal category enforce that linear variables cannot be duplicated, and the indexing ensures that dependent multiplicities are well-defined only when the dependency is on non-linear variables or appropriately guarded under W-types. We have added an appendix with outline proofs of subject reduction and linearity preservation, together with a sketch of how normalisation follows from the model. These additions directly address the interaction of dependent multiplicities with linear variables and recursion. revision: yes

  2. Referee: [Embedding and interaction rules] The embedding construction and interaction rules between the embedded linear logic and the host DTT are outlined in the abstract and introduction, but the paper does not provide detailed proof sketches or derivations showing that these rules yield a consistent quantitative typing system whose multiplicities correctly handle branching and recursion. Without this, the support for the main claim remains incomplete.

    Authors: The embedding is defined by interpreting linear types as objects in the linear fragment of the CwF while allowing multiplicities to be drawn from the host natural numbers, with interaction rules that substitute multiplicities only when the substituted term is non-linear. We have expanded Section 3 with a detailed derivation of the key interaction lemmas, including a proof sketch that branching (via dependent products) and recursion (via W-types) preserve the quantitative invariants. These sketches demonstrate that multiplicities remain well-defined and that no illicit duplication occurs. The Agda implementation further corroborates the rules by type-checking the provided examples. revision: yes

Circularity Check

0 steps flagged

No significant circularity in embedding-based construction of dependent multiplicities

full rationale

The paper derives its type system by embedding linear logic into dependent type theory, specifying interaction rules, and using the host natural numbers to obtain dependent multiplicities, with semantics characterized as CwFs indexed in symmetric monoidal categories generalizing Quantitative CwFs. This is a direct definitional construction rather than any reduction of a result to its inputs by construction, fitted parameters renamed as predictions, or load-bearing self-citation chains. The central claims about supporting W-types and resource annotations for branching/recursion follow from the embedding rules and do not presuppose the target system. The Agda implementation illustrates examples but is not invoked to close any definitional loop. The derivation is self-contained against external benchmarks of type theory embeddings.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim depends on the successful specification of interaction rules between embedded linear logic and the host dependent type theory, plus standard category-theoretic assumptions for the semantics.

axioms (2)
  • domain assumption Linear logic can be embedded into dependent type theory with specified interaction rules that preserve resource tracking.
    Invoked in the construction of the type system from the embedding.
  • domain assumption Natural numbers in the dependent type theory can be used to derive quantitative typing judgments.
    Used to obtain the multiplicity annotations.
invented entities (1)
  • Dependent multiplicities no independent evidence
    purpose: To annotate resource usage that varies with program variables for branching and recursion.
    New concept introduced to extend prior linear type theories.

pith-pipeline@v0.9.0 · 5668 in / 1297 out tokens · 47326 ms · 2026-05-22T00:24:38.490515+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages

  1. [1]

    Michael Gordon Abbott. 2003. Categories of containers. Ph. D. Dissertation. University of Leicester, UK

    work page 2003

  2. [2]

    Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for Pcf. Information and Computation 163, 2 (2000), 409–470. doi:10.1006/inco.2000.2930

    work page doi:10.1006/inco.2000.2930 2000

  3. [3]

    Samson Abramsky and Nikos Tzevelekos. 2011. Introduction To Categories and Categorical Logic . Springer, 3–94. doi:10.1007/978-3-642-12821-9_1

    work page doi:10.1007/978-3-642-12821-9_1 2011

  4. [4]

    2025.Principles of Dependent Type Theory

    Carlo Angiuli and Daniel Gratzer. 2025.Principles of Dependent Type Theory. in preparation. https://www.danielgratzer. com/papers/type-theory-book.pdf

    work page 2025

  5. [5]

    Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science LICS (2018), 56–65. doi:10.1145/3209108.3209189 , Vol. 1, No. 1, Article . Publication date: September 2025. 26 Maximilian Doré

    work page doi:10.1145/3209108.3209189 2018

  6. [6]

    Steve Awodey. 2018. Natural Models of Homotopy Type Theory. Mathematical Structures in Computer Science 28, 2 (2018), 241–286. doi:10.1017/S0960129516000268

    work page doi:10.1017/s0960129516000268 2018

  7. [7]

    Andrew Barber and Gordon Plotkin. 1996. Dual intuitionistic linear logic . Technical Report ECS-LFCS-96-347

    work page 1996

  8. [8]

    Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. 1997. The Coq Proof Assistant Reference Manual : Version 6.1 . Research Report RT-0203. INRIA. 214 pages. https:...

    work page 1997

  9. [9]

    P. N. Benton. 1995. A mixed linear and non-linear logic: Proofs, terms and models. In Computer Science Logic, Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 121–135

    work page 1995

  10. [10]

    Newton, Simon Peyton Jones, and Arnaud Spiwack

    Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2, POPL, Article 5 (Dec. 2017), 29 pages. doi:10.1145/3158093

    work page doi:10.1145/3158093 2017

  11. [11]

    Marc Bezem, Thierry Coquand, and Simon Huber. 2014. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 26) , Ralph Matthes and Aleksy Schubert (Eds.). 107–128. doi:10.4230/LIPIcs.TYPES.2013.107

    work page doi:10.4230/lipics.types.2013.107 2014

  12. [12]

    Edwin Brady. 2021. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 194) , Anders Møller and Manu Sridharan (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 9:1–9:26. doi:10.4230/ LIPIcs.ECOOP.2021.9

    work page 2021

  13. [13]

    Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. InCONCUR 2010 - Concurrency Theory, Paul Gastin and François Laroussinie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 222–236. doi:10. 1007/978-3-642-15375-4_16

    work page 2010

  14. [14]

    Iliano Cervesato and Frank Pfenning. 2002. A linear logical framework. Inforation and Computation 179, 1 (Nov. 2002), 19–75. doi:10.1006/inco.2001.2951

    work page doi:10.1006/inco.2001.2951 2002

  15. [15]

    Thierry Coquand. 1992. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks , Vol. 92. Citeseer, 66–79

    work page 1992

  16. [16]

    Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Proceedings of the 26th Annual ACM/IEEE Symposium on Logic in Computer Science LICS (2011), 133–142. doi:10.1109/LICS.2011.22

    work page doi:10.1109/lics.2011.22 2011

  17. [17]

    Nils Anders Danielsson. 2008. Lightweight semiformal time complexity analysis for purely functional data structures. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, California, USA) (POPL ’08). Association for Computing Machinery, New York, NY, USA, 133–144. doi:10. 1145/1328438.1328457

    work page arXiv 2008

  18. [18]

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover (system description). CADE (2015), 378–388. doi:10.1007/978-3-319-21401-6_26

    work page doi:10.1007/978-3-319-21401-6_26 2015

  19. [19]

    Valeria Correa Vaz de Paiva. 1990. The Dialectica Categories. Ph. D. Dissertation. University of Cambridge, UK

    work page 1990

  20. [20]

    Valeria Correa Vaz de Paiva. 1991. The Dialectica categories . Technical Report UCAM-CL-TR-213. University of Cambridge, Computer Laboratory. doi:10.48456/tr-213

    work page doi:10.48456/tr-213 1991

  21. [21]

    Maximilian Doré. 2025. Linear Types With Dynamic Multiplicities in Dependent Type Theory (Functional Pearl). Proc. ACM Program. Lang. 9, ICFP, Article 262 (2025), 21 pages. doi:10.1145/3747531 Note: forthcoming, preprint available at https://www.cs.ox.ac.uk/people/maximilian.dore/icfp25.pdf

    work page doi:10.1145/3747531 2025

  22. [22]

    Peter Dybjer. 1991. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics . Cambridge University Press, 280–306. doi:10.1017/CBO9780511569807.012

    work page doi:10.1017/cbo9780511569807.012 1991

  23. [23]

    Peter Dybjer. 1996. Internal type theory. In Types for Proofs and Programs (TYPES) 1995 , Stefano Berardi and Mario Coppo (Eds.). Springer, 120–134. doi:10.1007/3-540-61780-9_66

    work page doi:10.1007/3-540-61780-9_66 1996

  24. [24]

    Peter Dybjer. 1997. Representing Inductively Defined Sets By Wellorderings in Martin-Löf’s Type Theory. Theoretical Computer Science 176, 1 (1997), 329–335. doi:10.1016/S0304-3975(96)00145-4

    work page doi:10.1016/s0304-3975(96)00145-4 1997

  25. [25]

    Nicola Gambino and Martin Hyland. 2004. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 210–225. doi:10.1007/978-3-540-24849-1_14

    work page doi:10.1007/978-3-540-24849-1_14 2004

  26. [26]

    Jean-Yves Girard. 1987. Linear Logic. Theoretical computer science 50, 1 (1987), 1–101

    work page 1987

  27. [27]

    Martin Hyland and Andrea Schalk. 2003. Glueing and Orthogonality for Models of Linear Logic. Theoretical Computer Science 294, 1 (2003), 183–231. doi:10.1016/S0304-3975(01)00241-9 Category Theory and Computer Science

    work page doi:10.1016/s0304-3975(01)00241-9 2003

  28. [28]

    Krishnaswami, Pierre Pradic, and Nick Benton

    Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). Association for Computing Machinery, New York, NY, USA, 17–30. doi:10.1145/2676726.2676969

    work page doi:10.1145/2676726.2676969 2015

  29. [29]

    Joachim Lambek. 1958. The Mathematics of Sentence Structure. The American Mathematical Monthly 65, 3 (1958), 154–170. , Vol. 1, No. 1, Article . Publication date: September 2025. Dependent Multiplicities in Dependent Linear Type Theory 27

    work page 1958

  30. [30]

    Licata, Michael Shulman, and Mitchell Riley

    Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017. 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), Vol. 84) , Dale Miller (Ed.). Dagstuhl, Germany, 25:1–25:22. doi:10.4230/ LIPIcs....

    work page 2017

  31. [31]

    Per Martin-Löf. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium ’73, H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 73 – 118. doi:10.1016/S0049- 237X(08)71945-1

    work page doi:10.1016/s0049- 1975

  32. [32]

    Per Martin-Löf. 1982. Constructive Mathematics and Computer Programming. Studies in Logic and the Foundations of Mathematics 104 (1982), 153 – 175. https://dl.acm.org/doi/10.5555/3721.3731

    work page doi:10.5555/3721.3731 1982

  33. [33]

    Per Martin-Löf. 1984. Intuitionistic type theory . Bibliopolis

    work page 1984

  34. [35]

    Conor McBride and James McKinna. 2004. The View From the Left. Journal of Functional Programming 14, 1 (2004), 69–111. doi:10.1017/S0956796803004829

    work page doi:10.1017/s0956796803004829 2004

  35. [36]

    Paul-André Mellies. 2009. Categorical Semantics of Linear Logic. Panoramas et syntheses 27 (2009), 15–215

    work page 2009

  36. [37]

    Benjamin Moon, Harley Eades III, and Dominic Orchard. 2021. Graded Modal Dependent Type Theory. InProgramming Languages and Systems, Nobuko Yoshida (Ed.). Springer International Publishing, Cham, 462–490. doi:10.1007/978-3- 030-72019-3_17

    work page doi:10.1007/978-3- 2021

  37. [38]

    Moss and Tamara von Glehn

    Sean K. Moss and Tamara von Glehn. 2018. Dialectica models of type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford, United Kingdom) (LICS ’18). Association for Computing Machinery, New York, NY, USA, 739–748. doi:10.1145/3209108.3209207

    work page doi:10.1145/3209108.3209207 2018

  38. [39]

    Georgi Nakov and Fredrik Nordvall Forsberg. 2022. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 239) , Henning Basold, Jesper Cockx, and Silvia Ghilezan (Eds.). Dagstuhl, Germany, 10:1–10:22. doi:10.4230/LIPIcs.TYPES.2021.10

    work page doi:10.4230/lipics.types.2021.10 2022

  39. [40]

    Ulf Norell. 2007. Towards a practical programming language based on dependent type theory . Ph. D. Dissertation. Chalmers University of Technology and Göteborg University

    work page 2007

  40. [41]

    Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3, ICFP, Article 110 (July 2019), 30 pages. doi:10.1145/3341714

    work page doi:10.1145/3341714 2019

  41. [42]

    Pierre-Marie Pédrot. 2014. A functional functional interpretation. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science LICS/CSL (2014). doi:10.1145/2603088.2603094

    work page doi:10.1145/2603088.2603094 2014

  42. [43]

    Pierre-Marie Pédrot. 2024. Dialectica the Ultimate. (2024). https://www.p%C3%A9drot.fr/slides/tlla-07-24.pdf Talk at Trends in Linear Logic and Applications

    work page 2024

  43. [44]

    Mitchell Riley. 2022. A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory . Ph. D. Dissertation. Wesleyan University

    work page 2022

  44. [45]

    Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, and Max S. New. 2025. Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus. Proc. ACM Program. Lang. 9, PLDI, Article 178 (June 2025), 24 pages. doi:10.1145/3729281

    work page doi:10.1145/3729281 2025

  45. [46]

    Sam Staton. 2015. Algebraic Effects, Linearity, and Quantum Programming Languages. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). Association for Computing Machinery, New York, NY, USA, 395–406. doi:10.1145/2676726.2676999

    work page doi:10.1145/2676726.2676999 2015

  46. [47]

    The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Available at https://homotopytypetheory.org/book, Institute for Advanced Study

    work page 2013

  47. [48]

    Matthijs Vákár. 2015. A Categorical Semantics for Linear Logical Frameworks. In Foundations of Software Science and Computation Structures, Andrew Pitts (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 102–116. doi:10.1007/978- 3-662-46678-0_7

    work page doi:10.1007/978- 2015

  48. [49]

    Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2021. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming 31 (2021), e8. doi:10.1017/ S0956796821000034

    work page 2021

  49. [50]

    Kurt Von Gödel. 1958. Über Eine Bisher Noch Nicht benützte Erweiterung Des Finiten Standpunktes. Dialectica 12, 3-4 (1958), 280–287. doi:10.1111/j.1746-8361.1958.tb01464.x Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009 , Vol. 1, No. 1, Article . Publication date: September 2025

    work page doi:10.1111/j.1746-8361.1958.tb01464.x 1958