Markov's Principle for Propositional Type Theory

15 years 11 months ago

Download files.metaprl.org

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 speciﬁc 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.

Alexei Kopylov, Aleksey Nogin

Real-time Traffic

Automated Reasoning | Constructive Recursive Mathematics | Constructive Type Theory | CSL 2001 | Type Theory |

claim paper

Added	28 Jul 2010
Updated	28 Jul 2010
Type	Conference
Year	2001
Where	CSL
Authors	Alexei Kopylov, Aleksey Nogin

Sciweavers

Markov's Principle for Propositional Type Theory

Automated Reasoning | Constructive Recursive Mathematics | Constructive Type Theory | CSL 2001 | Type Theory |

Explore & Download

Productivity Tools

Sciweavers