<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class="">
<div class=""><font face="Courier" class="">=============================================================</font></div>
<div class=""><font face="Courier" class=""> CoqPL 2018</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class=""> Coq for Programming Languages</font></div>
<div class=""><font face="Courier" class=""> --</font></div>
<div class=""><font face="Courier" class=""> A Coq users and developers meeting</font></div>
<div class=""><font face="Courier" class=""> 13 January 2018, co-located with POPL (as usual)</font></div>
<div class=""><font face="Courier" class=""> Los Angeles, California, United States</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class=""> CALL FOR PARTICIPATIONS</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class=""> <a href="https://popl18.sigplan.org/track/CoqPL-2018" class="">
https://popl18.sigplan.org/track/CoqPL-2018</a></font></div>
<div class=""><font face="Courier" class="">=============================================================</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">Workshop Overview</font></div>
<div class=""><font face="Courier" class="">-----------------</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">The series of CoqPL workshops provide an opportunity for programming</font></div>
<div class=""><font face="Courier" class="">languages researchers to meet and interact with one another and</font></div>
<div class=""><font face="Courier" class="">members from the core Coq development team. At the meeting, we will</font></div>
<div class=""><font face="Courier" class="">discuss upcoming new features, see talks and demonstrations of</font></div>
<div class=""><font face="Courier" class="">exciting current projects, solicit feedback for potential future</font></div>
<div class=""><font face="Courier" class="">changes, and generally work to strengthen the vibrant community around</font></div>
<div class=""><font face="Courier" class="">our favourite proof assistant.</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">The exciting final progamme is now available at:</font></div>
<div class=""><font face="Courier" class=""><a href="https://popl18.sigplan.org/track/CoqPL-2018#program" class="">https://popl18.sigplan.org/track/CoqPL-2018#program</a></font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">Workshop Programme</font></div>
<div class=""><font face="Courier" class="">------------------</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">9:00-10:00: Keynote</font></div>
<div class=""><font face="Courier" class="">* CoqHammer: Strong Automation for Program Verification </font></div>
<div class=""><font face="Courier" class=""> Łukasz Czajka and Cezary Kaliszyk</font></div>
<div class=""><span class="Apple-tab-span" style="white-space:pre"><font face="Courier" class=""></font></span></div>
<div class=""><font face="Courier" class="">10:30-12:10: Tactics and Proof Engineering<span class="Apple-tab-span" style="white-space:pre">
</span></font></div>
<div class=""><font face="Courier" class="">* A “destruct” Tactic for Mtac2</font></div>
<div class=""><font face="Courier" class=""> Jan-Oliver Kaiser and Beta Ziliani</font></div>
<div class=""><font face="Courier" class="">* Typed Template Coq </font></div>
<div class=""><font face="Courier" class=""> Simon Boulier, Matthieu Sozeau, Nicolas Tabareau and Abhishek Anand</font></div>
<div class=""><font face="Courier" class="">* Elpi: an extension language for Coq </font></div>
<div class=""><font face="Courier" class=""> Enrico Tassi</font></div>
<div class=""><font face="Courier" class="">* Coqatoo: Generating Natural Language Versions of Coq Proofs </font></div>
<div class=""><font face="Courier" class=""> Andrew Bedford</font></div>
<div class=""><span class="Apple-tab-span" style="white-space:pre"><font face="Courier" class=""></font></span></div>
<div class=""><font face="Courier" class="">14:00-14:50: PL Metatheory<span class="Apple-tab-span" style="white-space:pre">
</span></font></div>
<div class=""><font face="Courier" class="">* Locally Nameless at Scale </font></div>
<div class=""><font face="Courier" class=""> Stephanie Weirich, Antoine Voizard and Anastasiya Kravchuk-Kirilyuk</font></div>
<div class=""><font face="Courier" class="">* A Coq Formalisation of a Core of R </font></div>
<div class=""><font face="Courier" class=""> Martin Bodin</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">14:50-15:30: Coq Deveveloprs Talk & Panel</font></div>
<div class=""><span class="Apple-tab-span" style="white-space:pre"><font face="Courier" class=""></font></span></div>
<div class=""><font face="Courier" class="">16:00-18:05: Semantics and Synthesis<span class="Apple-tab-span" style="white-space:pre">
</span></font></div>
<div class=""><font face="Courier" class="">* Revisiting Parametricity: Inductives and Uniformity of Propositions </font></div>
<div class=""><font face="Courier" class=""> Abhishek Anand and Greg Morrisett</font></div>
<div class=""><font face="Courier" class="">* Phantom Types for Quantum Programs </font></div>
<div class=""><font face="Courier" class=""> Robert Rand, Jennifer Paykin and Steve Zdancewic</font></div>
<div class=""><font face="Courier" class="">* Towards Context-Aware Data Refinement </font></div>
<div class=""><font face="Courier" class=""> Paul Krogmeier, Steven Kidd and Benjamin Delaware</font></div>
<div class=""><font face="Courier" class="">* Mechanizing the Construction and Rewriting of Proper Functions in Coq<span class="Apple-tab-span" style="white-space:pre">
</span></font></div>
<div class=""><font face="Courier" class=""> Edwin Westbrook</font></div>
<div class=""><font face="Courier" class="">* A calculus for logical refinements in separation logic </font></div>
<div class=""><font face="Courier" class=""> Dan Frumin and Robbert Krebbers</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">Contact</font></div>
<div class=""><font face="Courier" class="">-----------------</font></div>
<div class=""><font face="Courier" class=""><br class="">
</font></div>
<div class=""><font face="Courier" class="">For any queries, please contact : coqpl2018 at
<a href="http://easychair.org" class="">easychair.org</a></font></div>
</div>
<div class="">
<div style="color: rgb(0, 0, 0); font-variant-caps: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
<font face="Courier" class=""><br class="">
</font></div>
<div style="color: rgb(0, 0, 0); font-variant-caps: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
<font face="Courier" class="">Kind regards,</font></div>
<span style="color: rgb(0, 0, 0); font-variant-caps: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class=""><font face="Courier" class="">Yves
Bertot and Ilya Sergey</font></span></div>
<br class="">
</body>
</html>