Higher-Order Pushdown Trees are Circularly Computable

Abstract : We are interested in the problem of expressiveness of the following operations in the category of sets: finite products and coproducts, initial algebras (induction) and final coalgebras (coinduction). These operations are the building blocks of a logical system that allows circularity in Gentzen-style proofs. Proofs in this system are seen as simple programs, while the cut-elimination process is viewed as a running automaton with a memory device. In this paper, we show that higher-order trees, those accepted by higher-order pushdown automata, are computable in this setting, by providing an explicit simulation of the automata by cut-elimination.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01099127
Contributeur : David Baelde <>
Soumis le : mercredi 31 décembre 2014 - 15:22:02
Dernière modification le : jeudi 18 janvier 2018 - 02:05:58
Document(s) archivé(s) le : mercredi 1 avril 2015 - 10:11:11

Fichier

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

Identifiants

  • HAL Id : hal-01099127, version 1

Collections

Citation

Jérôme Fortier. Higher-Order Pushdown Trees are Circularly Computable. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉. 〈hal-01099127〉

Partager

Métriques

Consultations de la notice

73

Téléchargements de fichiers

52