POPL 2020 (series) / CoqPL 2020 (series) / The Sixth International Workshop on Coq for Programming Languages /
Towards Formally Verified Just-in-Time compilation
Sat 25 Jan 2020 15:35 - 16:05 at Maurepas - Contributed Talks & Coq Developers Chair(s): Joseph Tassarotti, Robbert Krebbers
Just-in-Time compilation consists in interleaving program interpretation and compilation at run-time, to achieve better performance than standard interpretation. While some of the execution time is spent compiling, a JIT compiler can leverage run-time information to make speculative optimizations. These optimizations create optimized versions of functions given some assumptions. While static compilers have been the topic of many formal verification works, few have tackled JIT compilation verification. We present our ongoing work about formal verification of a Just-in-Time compiler.
slides_coqpl20 (pres.pdf) | 834KiB |
(coqpl20-final5.pdf) | 360KiB |
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 |