Coq's Prolog and applications to defining semi-automatic tactics

Théo Zimmermann and Hugo Herbelin

TTT 2017 (workshop colocated with POPL)

Read the two-page abstract and the slides for the presentation.

This work is licensed under a Creative Commons Attribution 4.0 International License.