Alexei Kopylov, 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.
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.
Return to Alexei's Home Page