Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Wednesday, December 31, 2014 - 3:22:02 PM
Last modification on : Wednesday, October 7, 2020 - 3:14:59 AM
Long-term archiving on: : Wednesday, April 1, 2015 - 10:11:11 AM


Files produced by the author(s)


  • HAL Id : hal-01099127, version 1



Jérôme Fortier. Higher-Order Pushdown Trees are Circularly Computable. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099127⟩



Record views


Files downloads