What rocks in the new Rocq?

Prelegent(ci)

Jacek Chrząszcz

Afiliacja

MIMUW

Język referatu

angielski

Termin

17 października 2025 12:15

Pokój

p. 5450

Tytuł w języku polskim

Co w nowym Rocq-u?

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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...

---

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...

---