A cartesian closed category in Martin-Löf's intuitionistic type theory

DOI10.1016/S0304-3975(01)00309-7MaRDI QIDQ1853587zbMATH OpenOpenAlexFDO

Authors Silvio Valentini

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

zbMATH Keywords

Scott domains

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in artificial intelligence (68T27)

Recommendations

• Locally cartesian closed categories and type theory
• A type theoretic interpretation of constructive domain theory
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• scientific article; zbMATH DE number 2079044
• Constructive domain theory as a branch of intuitionistic pointfree topology

Cites work

• Constructive domain theory as a branch of intuitionistic pointfree topology
• Decidability in Intuitionistic Type Theory is Functionally Decidable
• Do-it-yourself type theory
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3780545 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1302065 (Why is no real title available?)
• scientific article; zbMATH DE number 1746890 (Why is no real title available?)
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(9)

• Constructive domain theory as a branch of intuitionistic pointfree topology
• Some points in formal topology.
• A type theoretic interpretation of constructive domain theory
• Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
• scientific article; zbMATH DE number 4010480 (Why is no real title available?)
• Internal diagrams and archetypal reasoning in category theory
• scientific article; zbMATH DE number 517016 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• A STUDY ON THE CARTESIAN CLOSED CATEGORY POSM

This page was built for publication: A cartesian closed category in Martin-Löf's intuitionistic type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853587)