What rocks in the new Rocq?

Speaker(s)

Jacek Chrząszcz

Affiliation

MIMUW

Language of the talk

English

Date

Oct. 17, 2025, 12:15 p.m.

Room

room 5450

Title in Polish

Co w nowym Rocq-u?

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

In the talk, we will present the latest changes in The Rocq Prover, formerly known as the Coq Proof Assistant. In particular, we will present new features of the prover, such as rewriting rules (at last! ;), and we will also discuss the changes made to existing components.
We will also share, from our own recent experience, the current stage of the renaming process, especially regarding the supporting tools...

---

Podczas seminarium opowiemy o najnowszych zmianach w The Rocq Prover, dawniej the Coq Proof Assistant. Przedstawimy w szczególności nowe elementy provera, takie jak reguły przepisywania (wreszcie ;), a także opowiemy o zmianach w elementach istniejących. Powiemy też z własnego niedawnego doświadczenia, na jakim etapie jest operacja zmiany nazwy, w szczególności jeśli chodzi o narzędzia wspomagające...

---