The independence of Markov's principle in type theory

DOI10.4230/LIPICS.FSCD.2016.17zbMATH Open1434.03137OpenAlexW2963610683MaRDI QIDQ5369482FDOQ5369482

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

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

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)

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
• Title not available (Why is that?)
• Russian constructivism in a prefascist theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)