POPL 2019 (series) / CoqPL 2019 (series) / The Fifth International Workshop on Coq for Programming Languages /
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.
Abstract (coqpl19-final9.pdf) | 70KiB |
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sat 19 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
16:00 - 17:40: Contributed Talks 4CoqPL at Sala VI Chair(s): Robbert KrebbersDelft University of Technology | |||
16:00 - 16:25 Talk | Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs CoqPL Qinxiang CaoShanghai Jiao Tong University File Attached | ||
16:25 - 16:50 Talk | Teaching Discrete Mathematics to Early Undergraduates with Software Foundations CoqPL File Attached | ||
16:50 - 17:15 Talk | Ltac2: Tactical Warfare CoqPL File Attached | ||
17:15 - 17:40 Talk | Towards a Coq Formalisation of Build Systems CoqPL File Attached |