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 (217KB), LNCS Entry

Slides from my 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.

Back to my publications

Last update: Thursday, March 14, 2002 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)