Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Speaker:Hugo Férée
coming from:University of Kent
Speakers Bio:
Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Wednesday, 22 November 2017
Duration:90 Minutes
Building:E1 5
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).
Name(s):Claudia Richter
Phone:9303 9103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:113
Tags, Category, Keywords and additional notes
Attachments, File(s):
Claudia Richter/MPI-SWS, 11/17/2017 10:17 AM
Last modified:
Uwe Brahm/MPII/DE, 11/22/2017 07:01 AM
  • Claudia Richter, 11/17/2017 10:24 AM -- Created document.