The Logic Seminar is a joint LOS/IMAR/ILDS seminar, featuring talks on mathematical logic, philosophical logic and logical aspects of computer science.
All seminars, except where otherwise indicated, will be on Thursdays between 14:00 and 16:00, Bucharest time. The seminars are held locally at Hall 214 (“Google”) of the Faculty of Mathematics and Computer Science, University of Bucharest, but can also be occasionally held remotely.
To receive announcements about the seminar, please send an email to logic-seminar@ilds.ro.
Organizers: Laurențiu Leuștean, Andrei Sipoș
Thursday, March 28, 2024
Gabriel Istrate (University of Bucharest)
Equilibria in multiagent online problems with predictions
Abstract:
We study the power of (competitive) algorithms with predictions in a multiagent setting. To this extent we introduce a multiagent version of the ski-rental problem. In this problem agents can collaborate by pooling resources to get a group licence for some asset. If the licence price is not met agents have to rent the asset individually for the day at a unit price. Otherwise the licence becomes available for everyone in perpetuity at no extra cost. Our main contribution is a best-response analysis of a single-agent competitive algorithm that assumes perfect knowledge of other agents’ actions (but no knowledge of its own renting time). We then give an analysis of the setting when agents have a predictor for their own active time, yielding a tradeoff between robustness and consistency. We investigate the effect of using such a predictor in an equilibrium, as well as the new equilibria formed in this way. This is joint work with Cosmin Bonchiș and Victor Bogdan (West University of Timișoara).
Thursday, April 4, 2024
Horațiu Cheval (University of Bucharest)
Partial (co)recursive functions in Coq and Lean
Abstract:
We present a novel method, based on domain theory, for defining partial recursive functions in interactive theorem provers like Coq and Lean, which would normally reject such definitions, as they require the termination of all functions. Our approach further extends to a representation of coinductive types and partial corecursive functions on them, which enhances the expressiveness of both systems. While Coq does contain built-in corecursion, it does not accept functions like mirror on infinitely deep trees, due to it violating the so-called guardedness condition, or filter on streams, as it is not total. Both of these can be defined in the presented encoding. Furthermore, Lean lacks entirely a native notion of coinductives, therefore the domain-theoretical representation can be used to build them from scratch in it. This is joint work with David Nowak and Vlad Rusu.
Past Seminars
- LOS/IMAR/ILDS Logic Seminar in 2022-2023
- LOS/IMAR/ILDS Logic Seminar in 2021-2022
- LOS/IMAR Logic Seminar in 2020-2021
- FMI/IMAR Logic Seminar in 2019-2020
- FMI/IMAR Logic Seminar in 2018-2019
- FMI/IMAR Logic Seminar in 2017-2018
- FMI/IMAR Logic Seminar in 2016-2017
- FMI/IMAR Logic Seminar in 2015-2016
- FMI/IMAR Logic Seminar in 2014-2015
- IMAR Logic Seminar in 2013-2014
- IMAR Logic Seminar in 2012-2013
- FMI Logic in Computer Science Seminar in 2014
- FMI Logic in Computer Science Seminar in 2013