A slower post, for the patient reader: Europrogramming. In the frenetic advance of AI and formal methods, it can be good to pause and reflect on where we come from and where we are going. 1/2

Europrogramming

Follow with Edit this page on Go back to the Bliki index

fabriziomontesi.com

📃 Excited to share progress on the 'Concurrency Challenge' of Dynamic Logic from our group! In our new ACM TOCL article (w/ Matteo Acclavio and Marco Peressotti), we integrate Propositional Dynamic Logic with Labelled Transition Systems (LTS) to obtain Operational Propositional Dynamic Logic (OPDL).

📃 Just accepted at ACM TOCL: a reconciliation of Linear Logic, the pi-calculus, and their metatheories. We (w/ Marco Peressotti) have developed a new semantics of linear logic that finally mends the gap between proofs and the expected behavioural theory of processes and session types. 1/

🎉 CSLib now includes a fully verified proof of the famous FLP (Fischer, Lynch and Paterson) result: it is impossible to achieve consensus in a distributed system with a faulty process and asynchronous messaging. Great work by Ching-Tsun Chou, which ... 1/2 #CSLib #FormalMethods #Lean #FORM

🌐 You can now play with CSLib directly in your browser at live.lean-lang.org! Many thanks to Robert Simmons for this! 👏 #Lean #CSLib #FormalMethods

📽️ Missed one of our CSLib General Meetings? You can now watch past meetings on the Lean FRO YouTube playlist: youtube.com/playlist?lis...

📣 Job alert: we're hiring PhDs and postdocs at FORM! Come work with us on formal methods, programming, verification, Lean, and #CSLib. We have many possible projects or you can propose your own. Deadline for applications: 16 August 2026 Links to the calls below.

🙏 Extremely thankful for and happy to welcome people stepping up to help with maintaining and reviewing contributions to CSLib. We have additions in areas including algorithms, automata, crypto, logic, monadic programming, programming languages, and machine learning. 1/

'Pact: A Choreographic Language for Agentic Ecosystems' develops a choreographic language with operations for agent choices and preferences, capturing important LLM interactions. Very nice! By Kiran Gopinathan, Jack Feser, Michelangelo Naim, Zenna Tavares, and Eli Bingham. 1/

Artificial Intelligence 🤝 Formal Methods Last week we had a very interesting online workshop with people from Mistral AI and FORM. 1/

👥 Save the date: CSLib Online Meetings Announcing the beginning of the CSLib online meetings, aimed at coordinating and facilitating the development of the library and its use. 1/

🔦 CSLib feature spotlight: fresh values. A great example of theory meeting practice. In many explanations of programs and proofs in computer science, you might find sentences like: - 'Pick a fresh value x not in the set' - 'For a fresh x' - 'Where x is a fresh name not in the program P' etc. 1/

🚀 CSLib is Growing – Follow Its Journey! The #Lean Computer Science Library (#CSLib) – a global effort to build reusable infrastructure for formal methods in AI-ready computer programming and research – is gaining momentum (>100 forks, >400 PRs, and nearly 500 stars on GitHub). (1/2)