A cartesian closed category in Martin-Löf's intuitionistic type theory
From MaRDI portal
Publication:1853587
DOI10.1016/S0304-3975(01)00309-7zbMath1018.68078MaRDI QIDQ1853587
Publication date: 21 January 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00309-7
68T27: Logic in artificial intelligence
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
Cites Work
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Do-it-yourself type theory
- Constructive domain theory as a branch of intuitionistic pointfree topology
- Decidability in Intuitionistic Type Theory is Functionally Decidable
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item