Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Watch a 51-minute conference talk from CoqPL 2025 where Enrico Tassi from INRIA introduces Elpi, a high-level programming language designed specifically for implementing commands and tactics for the Rocq prover. Learn how Elpi provides native support for syntax trees with binders and holes, eliminating the need to deal with complex De Bruijn indices and unification variables. Discover various Rocq extensions developed using Elpi that have gained widespread adoption. The presentation offers a gentle introduction to the Elpi programming language and its comprehensive API for Rocq interaction, surveys notable Elpi applications, and compares Elpi with other meta-languages, highlighting both advantages and limitations. This talk was presented at the CoqPL 2025 workshop on January 25, 2025, sponsored by ACM SIGPLAN.
