CoqPL 2018 The Fourth International Workshop on Coq for Programming Languages

About
Program

The series of CoqPL workshops provide an opportunity for programming languages researchers to meet and interact with one another and members from the core Coq development team. At the meeting, we will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes, and generally work to strengthen the vibrant community around our favorite proof assistant.

Topics in Scope

General purpose libraries and tactic language extensions
Domain-specific libraries for programming language formalization and verification
IDEs, profilers, tracers, debuggers, and testing tools
Reports on ongoing proof efforts conducted via (or in the context of) the Coq proof assistant
Experience reports from Coq usage in educational or industrial contexts

Workshop Format

The workshop format will be driven by you, members of the community. We will solicit abstracts for talks and proposals for demonstrations and flesh out format details based on responses. We expect the final program to include experiment reports, panel discussions, and invited talks (details TBA). Talks will be selected according to relevance to the workshop, based on the submission of an extended abstract.

To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop. However, presentations will be recorded and the videos made publicly available.

Previous Workshop Editions

CoqPL 2017 in Paris, France
CoqPL 2016 in St Petersburg, FL, USA
CoqPL 2015 in Mumbai, India

Accepted Talks

	Title
	A Coq Formalisation of a Core of R Martin Bodin File Attached
	A calculus for logical refinements in separation logic Dan Frumin, Robbert Krebbers File Attached
	A “destruct” Tactic for Mtac2 Jan-Oliver Kaiser, Beta Ziliani File Attached
	CoqHammer: Strong Automation for Program Verification Lukasz Czajka, Cezary Kaliszyk File Attached
	Coqatoo: Generating Natural Language Versions of Coq Proofs Andrew Bedford File Attached
	Elpi: an extension language for Coq Enrico Tassi File Attached
	Locally Nameless at Scale Stephanie Weirich, Antoine Voizard, Anastasiya Kravchuk-Kirilyuk File Attached
	Mechanizing the Construction and Rewriting of Proper Functions in Coq Edwin Westbrook File Attached
	Phantom Types for Quantum Programs Robert Rand, Jennifer Paykin, Steve Zdancewic File Attached
	Revisiting Parametricity: Inductives and Uniformity of Propositions Abhishek Anand, Greg Morrisett File Attached
	Session with the Coq Development Team Matthieu Sozeau, Maxime Dénès, Yves Bertot File Attached
	Towards Context-Aware Data Refinement Paul Krogmeier, Steven Kidd, Benjamin Delaware File Attached
	Typed Template Coq Simon Boulier, Matthieu Sozeau, Nicolas Tabareau, Abhishek Anand File Attached

Submission Guidelines

Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding the bibliography). We suggest formatting the text using the two-column ACM SIGPLAN latex style (9pt font). Templates are available from the ACM SIGPLAN page: http://www.sigplan.org/Resources/Author.