The Independence of Markov's Principle in Type Theory.
From MaRDI portal
Publication:5369482
DOI10.4230/LIPIcs.FSCD.2016.17zbMath1434.03137OpenAlexW2963610683MaRDI QIDQ5369482
Bassel Mannaa, Thierry Coquand
Publication date: 17 October 2017
Full work available at URL: https://dblp.uni-trier.de/db/conf/rta/fscd2016.html#CoquandM16
Metamathematics of constructive systems (03F50) Other aspects of forcing and Boolean-valued models (03E40) Type theory (03B38)
Related Items (7)
Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Unnamed Item ⋮ Canonicity for cubical type theory ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Higher order functions and Brouwer’s thesis ⋮ Formally computing with the non-computable
This page was built for publication: The Independence of Markov's Principle in Type Theory.
