Search

• < Previous
• 1
• Next >

---

The Independence of Markov's Principle in Type Theory

Thierry Coquand ; Bassel Mannaa.

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for&nbsp;[&hellip;]

---

Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory

Bassel Mannaa ; Rasmus Ejlers Møgelberg ; Niccolò Veltri.

Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to&nbsp;[&hellip;]

---