# Markov's Principle for Propositional Type Theory.

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)

## Abstract

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.