A two-level linear dependent type theory
From MaRDI portal
Cites work
- A framework for defining logics
- A linear logical framework
- Computational interpretations of linear logic
- Dependent ML An approach to practical programming with dependent types
- Guaranteeing safe destructive updates through a type system with uniqueness information for graphs
- scientific article; zbMATH DE number 1722663 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 591911 (Why is no real title available?)
- scientific article; zbMATH DE number 2003158 (Why is no real title available?)
- scientific article; zbMATH DE number 786485 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- I got plenty o' nuttin'
- Inductive families
- Integrating linear and dependent types
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Linear logic
- Linearity and uniqueness: an entente cordiale
- Operational interpretations of linear logic
- Program logics for certified compilers
- Purely Functional Data Structures
- Syntax and semantics of quantitative type theory
- The calculus of constructions
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- The Logic of Bunched Implications
This page was built for publication: A two-level linear dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7325543)
