Write a Blog >>

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.

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
30m
Talk
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
30m
Talk
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
15m
Break
Short break
CoqPL

16:50
45m
Demonstration
Session with the Coq Development Team
CoqPL