Enrico Tassi
where else to find them
what they talk about
where they keep going back
- CoqPL2 editions2021–2025
on a stage with
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Elpi: rule-based meta-languge for Rocq | CoqPL 2025 | 2025-01-25 |
Elpi is a rule-based meta-language that implements new Rocq commands and tactics by manipulating open terms with binders and holes, using higher-order abstract… | ||
| Practical and sound equality tests, automatically | CPP 2023 | 2023-01-16 |
A tool called feqb synthesizes sound equality tests and correctness proofs for Coq inductive types used with the Mathematical Components library, handling very… | ||
| Session with the Coq Development Team | CoqPL 2021 | 2021-01-19 |
Coq 8.13 appears: compile libraries with 8.13 to see new hint warnings and migrate by changing a hint’s attribute from global to export so it only activates… | ||
| Session with the Coq Development Team | POPL 2021 | 2021-01-17 |
Coq 8.13 ships with a new warning for hints and a staged migration: marking hints global preserves old behavior while the default will flip later, so compile… | ||
| nothing matches | ||