Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 16:50 - 17:15 at Sala VI - Contributed Talks 4 Chair(s): Robbert Krebbers

We present Ltac2, a proposal for the replacement of the Ltac tactic language that is shipped with Coq as the default interface to build up proofs interactively. Ltac2 is primarily motivated by two antagonistic desires, namely extending the expressivity and regularity of the historical tactic language of Coq while maintaining a strong backward compatibility. We thereafter give a bird’s eye view of the features and semantics of the current state of Ltac2.

Abstract (coqpl19-final9.pdf)70KiB

Sat 19 Jan

Displayed time zone: Belfast change