coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Sergey, Ilya" <i.sergey AT ucl.ac.uk>
- Subject: [Coq-Club] CoqPL'18: call for participations and final programme
- Date: Fri, 8 Dec 2017 14:17:34 +0000
- Accept-language: en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=i.sergey AT ucl.ac.uk; spf=None smtp.mailfrom=i.sergey AT ucl.ac.uk; spf=Pass smtp.helo=postmaster AT EUR02-AM5-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:IphvfxYOsMtDnJLeRo5tbhH/LSx+4OfEezUN459isYplN5qZpsm9bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i766D8JART5OkJJAaz7G4PWg4z3jLjzqNX9eQJN0XCGbKl9IQTy5STVp8Bcyd9jbL080BTEs1NVcOAQzGguOFHFzEW03du54JM2q3cYgPkm7cMVCv33
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
=============================================================
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
=============================================================
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:
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- [Coq-Club] CoqPL'18: call for participations and final programme, Sergey, Ilya, 12/08/2017
Archive powered by MHonArc 2.6.18.