Mon 8 Jan 2018 17:30 - 18:00 at Museum A - Proof Methods and Libraries Chair(s): René Thiemann

We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class \textsc{fp} of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.

Mon 8 Jan (GMT-07:00) Tijuana, Baja California change

CPP-2018
16:00 - 18:00: CPP 2018 - Proof Methods and Libraries at Museum A
Chair(s): René ThiemannUniversity of Innsbruck
CPP-201816:00 - 16:30
Talk
Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh
DOI
CPP-201816:30 - 17:00
Talk
Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington
DOI
CPP-201817:00 - 17:30
Talk
Niklas GrimmVienna University of Technology, Austria, Kenji MaillardInria Paris and ENS Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Matteo MaffeiSaarland University, Jonathan ProtzenkoMicrosoft Research, n.n., Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Santiago Zanella-BéguelinMicrosoft Research, n.n.
DOI
CPP-201817:30 - 18:00
Talk
Hugo FéréeUniversity of Kent, UK, Samuel HymUniversity of Lille, France, Micaela Mayero, Jean-Yves MoyenUniversity of Copenhagen, Denmark, David NowakCNRS, France
DOI