Ssreflect Users Discussion List

["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

Kind regards,

Yves Bertot and Ilya Sergey