Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 09:05 - 10:05 at Sala VI - Keynote & Contributed Talks 1 Chair(s): Ilya Sergey

As Coq approaches 35 years of history, the development of interactive proofs is more relevant than ever; crucial correctness properties can only be established mechanically with the help of humans, and the challenges that users and tooling face in the context of large-scale proofs are still considerable.

In this talk, I will try to explore Coq user interfaces from 3 different perspectives: first, we will survey past work. Many great ideas have been proposed over the years, however, implementation and maintenance have not always been a path of roses.

Understanding areas in need of improvement will lead us to the second part of the talk, where I will present SerAPI.

SerAPI aims to be a state-of-the-art language server for the Coq ecosystem. Special care has been put into its design to prevent maintenance and robustness problems. SerAPI provides an API for building and querying Coq documents, and has been successfully used by several projects.

While SerAPI works reasonably well today, is far from being a mature language server. In the final part of the talk, we will examine ongoing and future tooling work in the SerAPI/Coq roadmap. Some key issues are project management, incremental compilation, feature extraction, a enhanced display model, and support of standards such as the Language Server Protocol.

Sat 19 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote & Contributed Talks 1CoqPL at Sala VI
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
09:00
5m
Day opening
Opening
CoqPL

09:05
60m
Talk
Coq User Interfaces: Past, Present, and Future (Keynote)
CoqPL
10:05
25m
Talk
Counterexamples for Coq Conjectures
CoqPL
Samuel Gruetter Massachusetts Institute of Technology
File Attached