POPL 2020 (series) / CoqPL 2020 (series) / The Sixth International Workshop on Coq for Programming Languages /
A Coq Library of Undecidable Problems
Sat 25 Jan 2020 16:05 - 16:35 at Maurepas - Contributed Talks & Coq Developers Chair(s): Robbert Krebbers, Joseph Tassarotti
We propose a talk on our library of mechanised reductions to establish undecidability results in Coq. The library is a collaborative effort, growing constantly and we are seeking more outside contributors willing to work on undecidability results in Coq.
| (coqpl20-final6.pdf) | 354KiB |
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change
15:35 - 17:45 | Contributed Talks & Coq DevelopersCoqPL at Maurepas Chair(s): Robbert Krebbers Delft University of Technology, Joseph Tassarotti Boston College | ||
15:35 30mTalk | Towards Formally Verified Just-in-Time compilation CoqPL Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes- IRISA, David Pichardie Univ Rennes, ENS Rennes, IRISA File Attached | ||
16:05 30mTalk | A Coq Library of Undecidable Problems CoqPL Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA, Andrej Dudenhefner Saarland University, Edith Heiter Saarland University, Dominik Kirst Saarland University, Fabian Kunze Saarland University, Gert Smolka Saarland University, Simon Spies Saarland University, Dominik Wehr Saarland University, Universiteit van Amsterdam, Maximilian Wuttke Saarland University Media Attached File Attached | ||
16:35 15mBreak | Short break CoqPL | ||
16:50 45mDemonstration | Session with the Coq Development Team CoqPL | ||