Decidability in Intuitionistic Type Theory is Functionally Decidable

DOI10.1002/malq.19960420125zbMath0854.03008OpenAlexW2142989946MaRDI QIDQ4888341

Silvio Valentini

Publication date: 13 January 1997

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19960420125

zbMATH Keywords

decision functionMartin-Löf's intuitionistic type theoryintuitionistic decidable predicates

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Related Items (2)

Tychonoff's theorem in the framework of formal topologies ⋮ A cartesian closed category in Martin-Löf's intuitionistic type theory

Cites Work

• Unnamed Item
• Unnamed Item

This page was built for publication: Decidability in Intuitionistic Type Theory is Functionally Decidable