Ltac2: Tactical Warfare
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.
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
|16:00 - 16:25|
Qinxiang CaoShanghai Jiao Tong UniversityFile Attached
|16:25 - 16:50|
|16:50 - 17:15|
|17:15 - 17:40|