[TYPES/announce] CoqPL'18: call for participations and final programme

[Sergey, Ilya]

=============================================================
                         CoqPL 2018

                 Coq for Programming Languages
                             --
               A Coq users and developers meeting
           13 January 2018, co-located with POPL (as usual)
             Los Angeles, California, United States

                  CALL FOR PARTICIPATIONS

          https://popl18.sigplan.org/track/CoqPL-2018
=============================================================

Workshop Overview
-----------------

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 favourite proof assistant.

The exciting final progamme is now available at:
https://popl18.sigplan.org/track/CoqPL-2018#program

Workshop Programme
------------------

9:00-10:00: Keynote
* CoqHammer: Strong Automation for Program Verification
  Łukasz Czajka and Cezary Kaliszyk
10:30-12:10: Tactics and Proof Engineering
* A “destruct” Tactic for Mtac2
  Jan-Oliver Kaiser and Beta Ziliani
* Typed Template Coq
  Simon Boulier, Matthieu Sozeau, Nicolas Tabareau and Abhishek Anand
* Elpi: an extension language for Coq
  Enrico Tassi
* Coqatoo: Generating Natural Language Versions of Coq Proofs
  Andrew Bedford
14:00-14:50: PL Metatheory
* Locally Nameless at Scale
  Stephanie Weirich, Antoine Voizard and Anastasiya Kravchuk-Kirilyuk
* A Coq Formalisation of a Core of R
  Martin Bodin

14:50-15:30: Coq Deveveloprs Talk & Panel
16:00-18:05: Semantics and Synthesis
* Revisiting Parametricity: Inductives and Uniformity of Propositions
  Abhishek Anand and Greg Morrisett
* Phantom Types for Quantum Programs
  Robert Rand, Jennifer Paykin and Steve Zdancewic
* Towards Context-Aware Data Refinement
  Paul Krogmeier, Steven Kidd and Benjamin Delaware
* Mechanizing the Construction and Rewriting of Proper Functions in Coq
  Edwin Westbrook
* A calculus for logical refinements in separation logic
  Dan Frumin and Robbert Krebbers

Contact
-----------------

For any queries, please contact : coqpl2018 at easychair.org<http://easychair.org>

Kind regards,
Yves Bertot and Ilya Sergey

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20171208/74d32d3b/attachment-0001.html>