A cartesian closed category in Martin-Löf's intuitionistic type theory
From MaRDI portal
Publication:1853587
DOI10.1016/S0304-3975(01)00309-7zbMath1018.68078OpenAlexW1993848174MaRDI 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
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
This page was built for publication: A cartesian closed category in Martin-Löf's intuitionistic type theory
