All Outputs (2)

Contractive Functions on Infinite Data Structures (2016)
Conference Proceeding
Capretta, V., Hutton, G., & Jaskelioff, M. (2016). Contractive Functions on Infinite Data Structures. In IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages (1-13). https://doi.org/10.1145/3064899.3064900

Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they... Read More about Contractive Functions on Infinite Data Structures.

A coalgebraic view of bar recursion and bar induction (2016)
Journal Article
Capretta, V., & Uustalu, T. (2016). A coalgebraic view of bar recursion and bar induction. Lecture Notes in Artificial Intelligence, 9634, 91-106. https://doi.org/10.1007/978-3-662-49630-5_6

We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover certain classically valid theorems in a constructive setting... Read More about A coalgebraic view of bar recursion and bar induction.