Research Repository

See what's under the surface


The coinductive formulation of common knowledge (2018)
Conference Proceeding
Baston, C., & Capretta, V. (2018). The coinductive formulation of common knowledge. In Interactive theorem proving; Lecture Notes in Computer Science, 126-141. doi:10.1007/978-3-319-94821-8_8

We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rathe... Read More

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, doi:10.1007/978-3-662-49630-5_6. ISSN 0302-9743

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