Anne Baanen

I'm in the news!

https://vu.nl/en/news/2024/phd-degree-awarded-to-anne-baanen

New paper! I am happy to announce the publication of the paper "Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge" by Kai Obendrauf, Anne Baanen, Patrick Koopmann, and Vera Stebletsova.

https://doi.org/10.4230/LIPIcs.ITP.2024.28

Coalition Logic (CL) is a well-known formalism for reasoning about the strategic abilities of groups of agents in multi-agent systems. Coalition Logic with Common Knowledge (CLC) extends CL with operators from epistic logics, and thus with the ability to model the individual and common knowledge of agents. We have formalized the syntax and semantics of both logics in the interactive theorem prover Lean 4, and used it to prove soundness and completeness of its axiomatization. Our formalization uses the type class system to generalize over different aspects of CLC, thus allowing us to reuse some of to prove properties in related logics such as CL and CLK (CL with individual knowledge).

I co-supervised Kai's master thesis and they produced an amazing amount of high-quality work. I'm very glad to have been around during the process and do my bit to make a nice paper for their results.

Can I ask how things are going with the Coq → Rocq rename? Last I heard a couple months ago they were sorting out some legal issues. Hopefully those didn't cancel the whole project!

The Fondation Sciences Mathématiques de Paris launches a call for PhD candidates *who are not currently based in France* to apply for fellowships in mathematical sciences, under the condition that they are followed by two co-supervisors, one in the Paris area and one outside. The deadline for applying is February 14th, and if the first step is passed there are two more months to find the tandem of researchers that would supervise the PhD. Students coming from the UK are eligible both at the end of their 4th or 5th year. If anyone is interested to work with Riccardo Brasca and Filippo A.E. Nuccio, feel free to contact them (either on the Lean community Zulip chat or at riccardo.brasca@gmail.com / filippo.nuccio@univ-st-etienne.fr).

Jim Portegies, Paige North, and Johan Commelin are looking for a PhD student to work on the development of proof assistants for education such as Waterproof [1] (see [2] for a project description). The position will be based at the University of Utrecht (though it will also include collaboration with the Technical University of Eindhoven) and will start in Fall 2024. We will consider applications until the position has been filled, so please contact one of the project members soon if you are interested. You can reach Johan via Zulip DM or at j.m.commelin@uu.nl.

[1] https://impermeable.github.io

[2] https://paigenorth.github.io/tue-uu-project.pdf

i think i made an oopsie and replaced the main database with an older dump. let me see if i can fix it before i fall asleep!

(Worst case is we'll just have to repost our best posts of the last month or so!)

This is a very cool project that got open sourced recently: a symbolic evaluator for ARMv8 in Lean! https://github.com/leanprover/LNSym

Tomorrow at the GPN event in Karlsruhe:
https://cfp.gulas.ch/gpn22/talk/WWMGVN/

Intro to Lean 4: A language at the intersection of programming and mathematics
31.05, 14:30–15:30 (Europe/Berlin), ZKM Vortragssaal
Sprache: English

Type theory is the secret sauce that makes a programming language awesome. The more knowledge we can make the compiler aware of, the more we can rely on the compiler.

But what is the limit? What if we could take make bad state unrepresentable to the mathematical extreme? What is a proof anyway, can you eat it? Come on a wonderful journey into the land of dependent types, where we try building type-safe SQL queries, and sweeten the deal with our own syntactic sugar.

Should be live streamed at https://streaming.media.ccc.de/gpn22

At the ILLC in Amsterdam, Balder ten Cate is offering a PhD position on Machine Learning for Automated Reasoning. See here for the offer. The deadline for applications is 11 March 2024 and they plan to interview candidates in April. For any questions you may have, please contact Balder at b.d.tencate@uva.nl.

[PhD position on the Leanprover Zulip chat:](https://leanprover.zulipchat.com/#narrow/channel/284757-job-postings/topic/PhD.20position.20in.20Saint-.C3.89tienne.26Paris)

> Dear All, Riccardo Brasca and I (Filippo Nuccio) are looking for a PhD student to work on formalization of advanced number theory or some functional analysis (either nonarchimedean or aspects of pp-Banach spaces that showed up in the LTE). The position will be based at the University of Saint-Étienne and it will include collaboration with the Université Paris Cité, will start in Fall 2025 and last 3 years. Please contact one of us if you are interested, either here via Zulip DM or at filippo.nuccio@univ-st-etienne.fr or riccardo.brasca@gmail.com. The deadline for application is April 18th, but we'd like to get in touch with interested candidates as soon as possible.

We are hiring!

In the [Software and Sustainability Research Group (S2 Group)](https://s2group.cs.vu.nl/) at Vrije Universiteit Amsterdam we are looking for synergetic and ambitious candidates for a career track position as assistant professor in software architecture. Because we target gender balance in our department, this position is opened in the context of the Lovelace Fellowship Programme (more info at [Lovelace Fellowship](https://vu.nl/en/about-vu/more-about/lovelace-fellowship-programme-for-gender-diversity)).

Vacancy info and applications: https://workingat.vu.nl/vacancies/assistant-professor-career-track-software-architecture-amsterdam-1058250

Deadline: 5-may-2024

Join us! Questions about the vacancy? Drop an email to Patricia Lago p.lago@vu.nl

> We are pleased to announce the International Logic Olympiad 2024 (ILO2024) a world-wide contest on Logic for high school students.
>
> Register & learn more at https://www.logicolympiad.org/
> Brief Overview: http://intrologic.stanford.edu/olympiad/introduction.php