An intuitionistic logic that proves Markov's principle

Hugo Herbelin 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov's principle suited for predicate logic. At the computational level, the extraction of an existential witness out of a proof of its double negation is done by using a form of statically-bound exception mechanism, what can be seen as a direct-style variant of Friedman's A-translation.
Type de document :
Communication dans un congrès
Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. IEEE Computer Society, pp.50-56, 2010, Proceedings, 25th Annual IEEE Symposium on Logic in Computer Science (LICS '10), Edinburgh, UK, 11-14 July 2010
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00481815
Contributeur : Hugo Herbelin <>
Soumis le : vendredi 7 mai 2010 - 13:35:25
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 14:30:51

Fichier

herbelin.LICS2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00481815, version 1

Collections

Citation

Hugo Herbelin. An intuitionistic logic that proves Markov's principle. Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. IEEE Computer Society, pp.50-56, 2010, Proceedings, 25th Annual IEEE Symposium on Logic in Computer Science (LICS '10), Edinburgh, UK, 11-14 July 2010. 〈inria-00481815〉

Partager

Métriques

Consultations de la notice

370

Téléchargements de fichiers

147