Campus Event Calendar
Event Entry
What and Who
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée
University of Kent
SWS Colloquium
SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 22 November 2017
10:30
90 Minutes
E1 5
029
Saarbrücken
Abstract
Formal reasoning about computational complexity turns out to be quite cumbersome as it often requires to manipulate explicit time bounds for a specific machine model. Implicit Computational Complexity is a research area which provides techniques and complexity classes characterisations to avoid this. We have formally verified the soundness (and part of the completeness) of such a technique − called quasi-interpretations − using the Coq proof assistant. In particular, we turned this into a tool to
help guarantee the polynomial complexity of programs (here, term rewriting systems).
help guarantee the polynomial complexity of programs (here, term rewriting systems).
Contact
Claudia Richter
9303 9103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
113
passcode not visible
logged in users only
Claudia Richter, 11/17/2017 10:24 -- Created document.