Sergey, Ilya
2017-12-08 14:17:34 UTC
=============================================================
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
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