Alexei Kopylov and Aleksey Nogin.
Markov's principle for propositional type theory.
In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science, pages 570-584. Springer-Verlag, 2001:
PDF (216 KB), PostScript (217 KB), LNCS Entry
Slides from the CSL'01 presentation: PostScript (220KB)
In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov's principle from constructive recursive mathematics. Markov's principle is especially useful for proving termination of specific computations. Allowing a limited form of classical reasoning we get more powerful resulting system which remains constructive and valid in the standard constructive semantics of a type theory. We also show that this principle can be formulated and used in a propositional fragment of a type theory.