The independence of Markov's principle in type theory

DOI10.4230/LIPICS.FSCD.2016.17MaRDI QIDQ5369482zbMATH OpenOpenAlexFDO

Authors Thierry Coquand, Bassel Mannaa

Publication date 17 October 2017

Full work available at URL https://dblp.uni-trier.de/db/conf/rta/fscd2016.html#CoquandM16

zbMATH Keywords

Cantor spaceforcingMarkov's principledependent type theory

Mathematics Subject Classification ID

Other aspects of forcing and Boolean-valued models (03E40) Metamathematics of constructive systems (03F50) Type theory (03B38)

Recommendations

• The independence of Markov's principle in type theory
• scientific article; zbMATH DE number 1841844
• On a weakening of Markov's Principle
• scientific article; zbMATH DE number 5364051
• Markov's rule revisited

Cited in

(12)

• Canonicity for cubical type theory
• Call-by-value lambda calculus as a model of computation in Coq
• Failure is not an option. An exceptional type theory
• Formally computing with the non-computable
• The independence of Markov's principle in type theory
• Constructive and mechanised meta-theory of intuitionistic epistemic logic
• scientific article; zbMATH DE number 7215286 (Why is no real title available?)
• Russian constructivism in a prefascist theory
• scientific article; zbMATH DE number 1841844 (Why is no real title available?)
• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• Higher order functions and Brouwer's thesis
• Weak call-by-value lambda calculus as a model of computation in Coq

This page was built for publication: The independence of Markov's principle in type theory

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