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

CoqPL-2019
16:00 - 17:40: CoqPL - Contributed Talks 4 at Sala VI
Chair(s): Robbert KrebbersDelft University of Technology
CoqPL-201916:00 - 16:25
Talk
File Attached
CoqPL-201916:25 - 16:50
Talk
Michael GreenbergPomona College, Joseph C. OsbornPomona College
File Attached
CoqPL-201916:50 - 17:15
Talk
File Attached
CoqPL-201917:15 - 17:40
Talk
Georgy LukyanovNewcastle University, UK, Andrey MokhovNewcastle University, UK
File Attached