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
(217KB), LNCS
Entry
Slides from my 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.
Last update: Thursday, March 14, 2002 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)