Syntax and semantics of quantitative type theory
From MaRDI portal
Publication:5145276
DOI10.1145/3209108.3209189zbMATH Open1452.03029OpenAlexW2799182172MaRDI QIDQ5145276FDOQ5145276
Authors: 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/
Recommendations
Cited In (22)
- When programs have to watch paint dry
- A framework for substructural type systems
- Linear Dependent Type Theory for Quantum Programming Languages
- A Java-like calculus with heterogeneous coeffects
- A quantitative interpretation of Girard's System F
- \( \pi\) with leftovers: a mechanisation in Agda
- Quantifiers on languages and codensity monads
- Generalized bounded linear logic and its categorical semantics
- Graded modal dependent type theory
- Additive types in quantitative type theory
- Title not available (Why is that?)
- Quantitative Information Flow, Relations and Polymorphic Types
- Quantitative global memory
- Extracting functional programs from Coq, in Coq
- Logical foundations of quantitative equality
- A dependent dependency calculus
- Title not available (Why is that?)
- Builtin types viewed as inductive families
- Impredicative encodings of inductive-inductive data in Cedille
- Type-safe quantum programming in Idris
- Monotone recursive types and recursive data representations in Cedille
- Complexity of Grammar Induction for Quantum Types
This page was built for publication: Syntax and semantics of quantitative type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145276)
