All Outputs (5)

Game Forms for Coalition Effectivity Functions (2019)
Presentation / Conference Contribution
Baston, C., & Capretta, V. (2019, June). Game Forms for Coalition Effectivity Functions. Presented at 25th International Conference onTypes for Proofs and Programs (TYPES 2019), Oslo, Norway

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)
Presentation / Conference Contribution
Baston, C., & Capretta, V. (2018, October). The Coinductive Formulation of Common Knowledge. Presented at ITP 2018 - Interactive Theorem Proving, Oxford, United Kingdom

© 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)
Presentation / Conference Contribution
Capretta, V., & Fowler, J. (2017, June). The continuity of monadic stream functions. Presented at 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland

© 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)
Presentation / Conference Contribution
Capretta, V., Hutton, G., & Jaskelioff, M. (2016, August). Contractive Functions on Infinite Data Structures. Presented at 28th Symposium on Implementation and Application of Functional Languages, Leuven, Belgium

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.