A cartesian closed category in Martin-Löf's intuitionistic type theory
- 1 January 2003
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 290 (1) , 189-219
- https://doi.org/10.1016/s0304-3975(01)00309-7
Abstract
No abstract availableKeywords
This publication has 4 references indexed in Scilit:
- Extensionality Versus ConstructivityMathematical Logic Quarterly, 2002
- Constructive domain theory as a branch of intuitionistic pointfree topologyTheoretical Computer Science, 1996
- Decidability in Intuitionistic Type Theory is Functionally DecidableMathematical Logic Quarterly, 1996
- Do-it-yourself type theoryFormal Aspects of Computing, 1989