Reference. Integrating Linear and Dependent Types

Neel Krishnaswami, Cécilia Pradic, Nick Benton · POPL · 2015 · linear-logic type-theory · PDF · DOI · pldb
In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.

Cite
Cite as @krishnaswami_integrating_2015 (helia, typst) · \cite{krishnaswami_integrating_2015} (LaTeX)
BibTeX
bibtex · 16 lines
@inproceedings{krishnaswami_integrating_2015,
 title = {Integrating {Linear} and {Dependent} {Types}},
 author = {Krishnaswami, Neelakantan R. and Pradic, Cécilia and Benton, Nick},
 year = {2015},
 isbn = {978-1-4503-3300-9},
 doi = {10.1145/2676726.2676969},
 url = {https://dl.acm.org/doi/10.1145/2676726.2676969},
 urldate = {2024-01-04},
 booktitle = {Proceedings of the 42nd {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
 pages = {17--30},
 publisher = {ACM},
 address = {Mumbai India},
 month = {January},
 language = {en},
 abstract = {In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.}
}
hayagriva YAML (typst)
yaml · 22 lines
krishnaswami_integrating_2015:
  type: article
  title: Integrating {Linear} and {Dependent} {Types}
  author:
  - Krishnaswami, Neelakantan R.
  - Pradic, Cécilia
  - Benton, Nick
  date: 2015-01
  page-range: 17-30
  url:
    value: https://dl.acm.org/doi/10.1145/2676726.2676969
    date: 2024-01-04
  serial-number:
    doi: 10.1145/2676726.2676969
    isbn: 978-1-4503-3300-9
  abstract: In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.
  parent:
    type: proceedings
    title: Proceedings of the 42nd {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}
    publisher:
      name: ACM
      location: Mumbai India
Download: krishnaswami_integrating_2015.bib · krishnaswami_integrating_2015.yml
Cited by (13)

Impredicativity in Linear Dependent Type Theory speight-2026-impredicativityarXiv · 2026
We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.
arXiv

One Weird Trick to Untie Landin’s Knot koronkevich-2025-onearXiv · 2025
In this work, we explore Landin’s Knot, which is understood as a pattern for encoding general recursion, including non-termination, that is possible after adding higher-order references to an otherwise terminating language. We observe that this isn’t always true – higher-order references, by themselves, don’t lead to non-termination. The key insight is that Landin’s Knot relies not primarily on references storing functions, but on unrestricted quantification over a function’s environment. We show this through a closure converted language, in which the function’s environment is made explicit and hides the type of the environment through impredicative quantification. Once references are added, this impredicative quantification can be exploited to encode recursion. We conjecture that by restricting the quantification over the environment, higher-order references can be safely added to terminating languages, without resorting to more complex type systems such as linearity, and without restricting references from storing functions.
arXiv

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek𝙳), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek𝙳, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek𝙳 using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

Foundations of Substructural Dependent Type Theory aberle-2024-foundationsarXiv · 2024
This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on this front has generally managed to deliver type systems possessing either syntax or semantics inclusive of certain practical applications, but has struggled to combine these all in one and the same system. Toward resolving this difficulty, I propose a novel categorical interpretation of substructural dependent types, analogous to the use of monoidal categories as models of linear and ordered logic, that encompasses a wide class of mathematical and computational examples. On this basis, I develop a general framework for substructural dependent type theories, and proceed to prove some essential metatheoretic properties thereof. As an application of this framework, I show how it can be used to construct a type theory that satisfactorily addresses the problem of effectively representing cut admissibility for linear sequent calculus in a logical framework.
arXiv

Polynomial Time and Dependent Types atkey-2024-polynomialPOPL · 2024
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory .
PDF · DOI · arXiv · pldb

Dependent Type Refinements for Futures somayyajula-2023-dependentENTCS · 2023
Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based process calculus that arises from the Curry-Howard interpretation of the intuitionistic semi-axiomatic sequent calculus and includes unrestricted recursion both at the level of types and processes. With our type refinement system, we can reason about the partial correctness of SAX programs, complementing prior work on sized type refinements that supports reasoning about termination. Our design regime synthesizes the infinitary proof theory of SAX with that of bidirectional typing and Hoare logic, deriving some standard reasoning principles for data and (co)recursion while enabling information hiding for codata. We prove syntactic type soundness, which entails a notion of partial correctness that respects codata encapsulation. We illustrate our language through a few simple examples.
DOI

A two-level linear dependent type theory fu2023twolevellineardependenttypearXiv · 2023
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean. Additionally, programs can be freely reflected into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource safe programs and verify their correctness using a unified language.
Web · arXiv

A Formal Logic for Formal Category Theory new_licata_2023FoSSaCS · 2023
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category-theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model in virtual equipments, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.
DOI

Quantitative Polynomial Functors nakov_quantitative_2022TYPES · 2022
We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.
DOI

Fractional Types: Expressive and Safe Space Management for Ancilla Bits chen-2020-fractionalRC · 2020
DOI · arXiv

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntaxLICS · 2018
DOI

Substructural calculi with dependent types luo2018

In this paper, we investigate how to introduce dependent types into the substructural calculi such as the Lambek calculus and linear logic. The motivations of such a move include facilitating a closer correspondence between syntax and semantics in natural language analysis and developing promising applications such as that to concurrency through dependent session types.

We shall present two substructural calculi with dependent types: the first containing dependent Lambek types and the second dependent linear types. Technically, the former adheres to the usual assumption that types do not depend on substructural variables (in this case, the Lambek variables), which makes the technical development easier, while the latter allows type dependency on linear variables, which makes the development more challenging as well as more interesting in applications.

DOI

I Got Plenty o’ Nuttin’ mcbride-2016-iA List of Successes That Can Change the World · 2016
DOI
Cites 45 works (8 here)
With notes (8)

On the unity of duality zeilberger-2008-onAPAL · 2008
DOI

Observational equality, now! altenkirch-2007-observationalPLPV · 2007
DOI

Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalueSemantic Structures in Computation · 2003
DOI

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002
In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
DOI

A judgmental reconstruction of modal logic pfenning-2001-aMSCS · 2001
DOI

The logic of bunched implications ohearn_pym_bi_1999BSL · 1999
We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI’s proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers [inline image] and [inline image] which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995CSL · 1995
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.
DOI

Linear logic girard_linear_1987TCS · 1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (37)
krishnaswami_integrating_2015 reference entries/refs/krishnaswami_integrating_2015/krishnaswami_integrating_2015.hel