Syntax and Semantics of Quantitative Type Theory

DOI10.1145/3209108.3209189zbMath1452.03029OpenAlexW2799182172MaRDI QIDQ5145276

Robert Atkey

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://strathprints.strath.ac.uk/64031/

zbMATH Keywords

linear logictype theory

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Type theory (03B38)

Related Items (14)

Linear Dependent Type Theory for Quantum Programming Languages ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Extracting functional programs from Coq, in Coq ⋮ When programs have to watch paint dry ⋮ Additive types in quantitative type theory ⋮ A framework for substructural type systems ⋮ A dependent dependency calculus ⋮ A Java-like calculus with heterogeneous coeffects ⋮ Quantitative global memory ⋮ Unnamed Item ⋮ Generalized bounded linear logic and its categorical semantics ⋮ Graded modal dependent type theory ⋮ Unnamed Item ⋮ \( \pi\) with leftovers: a mechanisation in Agda

This page was built for publication: Syntax and Semantics of Quantitative Type Theory