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): Joseph Tassarotti, Robbert Krebbers
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 Jan Times are displayed in time zone: Saskatchewan, Central America change
Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change
15:35 - 17:45: Contributed Talks & Coq DevelopersCoqPL at Maurepas Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology | |||
| 15:35 - 16:05 Talk | Towards Formally Verified Just-in-Time compilation CoqPL Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA File Attached | ||
| 16:05 - 16:35 Talk | A Coq Library of Undecidable Problems CoqPL Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA, Andrej DudenhefnerSaarland University, Edith HeiterSaarland University, Dominik KirstSaarland University, Fabian KunzeSaarland University, Gert SmolkaSaarland University, Simon SpiesSaarland University, Dominik WehrSaarland University, Universiteit van Amsterdam, Maximilian WuttkeSaarland University Media Attached File Attached | ||
| 16:35 - 16:50 Break | Short break CoqPL | ||
| 16:50 - 17:35 Demonstration | Session with the Coq Development Team CoqPL | ||