# * Markov's Principle For Propositional Type Theory *

## by Alexei Kopylov, Aleksey Nogin

2001

Proceedings of the 10 th Annual Conference of the EACSL

- unofficial copies PDF

**Abstract**

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.

**bibTex ref: KN01**

cite link