Campus Event Calendar
Event Entry
New for: D3
What and Who
Markov's principle for propositional type theory
Alexey Nogin
Cornell University
Talk
AG 1, AG 2, AG 3, AG 4
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 25 September 2001
16:15
-- Not specified --
46.1 - MPII
024
Saarbrücken
Abstract
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 (Cornell).
Contact
--email hidden
passcode not visible
logged in users only