KnowledgeBase » SEMINAR » ID = 578

Markov's Principle for Propositional Type Theory

by Aleksey Nogin
2001-2002

I will give a practice presentation of the talk I am planning to give at CSL. All are welcome, and comments are appreciated. In my talk I will show how to extend a computational 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. I will also show that this principle can be formulated and used in a propositional fragment of a type theory.
This work is joint with Alexei Kopylov.