Skip to main content

Research Repository

Advanced Search

All Outputs (5)

Game Forms for Coalition Effectivity Functions (2019)
Conference Proceeding
Baston, C., & Capretta, V. (2019). Game Forms for Coalition Effectivity Functions. In N. van der Weide, & M. Bezem (Eds.), 25th International Conference onTypes for Proofs and Programs (TYPES 2019), 26-27

Introduction Coalition logic, introduced by Pauly, 1 is a multi-agent modal logic for reasoning about what groups of agents can achieve if they act collectively, as a coalition. The semantics for coalition logic is based on game forms, which are esse... Read More about Game Forms for Coalition Effectivity Functions.

The Coinductive Formulation of Common Knowledge (2018)
Conference Proceeding
Baston, C., & Capretta, V. (2018). The Coinductive Formulation of Common Knowledge. https://doi.org/10.1007/978-3-319-94821-8_8

© 2018, Springer International Publishing AG, part of Springer Nature. 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 e... Read More about The Coinductive Formulation of Common Knowledge.

The continuity of monadic stream functions (2017)
Conference Proceeding
Capretta, V., & Fowler, J. (2017). The continuity of monadic stream functions. In Proceedings - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) (658-669). https://doi.org/10.1109/LICS.2017.8005119

© 2017 IEEE. Brouwer's continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that... Read More about The continuity of monadic stream functions.

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.