Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Computational content of circular proof systems
du groupe Séminaire Méthodes Formelles

Date 2020-01-21  07:00-07:00
TitreComputational content of circular proof systems 
RésuméCyclic proofs are a class of formal proof systems that allow some kind of circular reasoning. Unlike classical proofs, represented by finite trees with axioms as leaves, cyclic proofs are represented by trees containing infinite branches. The Curry-Howard correspondence allows us to see these cyclic proofs as programs. We investigate the computational content of a cyclic proof system based on Kleene algebra, where we see expressions as data types. Different proofs of the same sequent e |- f can be interpreted as different programs mapping every input of type e to an output of type f. We show that depending on the particular rules allowed in the system, the computational content of proofs matches different known complexity classes: regular languages, LogSpace, primitive recursive functions, system T. Various tools are used to pinpoint these different expressive powers, including a newly introduced class of automata (Jumping Multihead Automata), and results from the field of reverse mathematics. This is joint work with Laureline Pinault, Damien Pous, and Anupam Das. 
Lieu178 
OrateurDenis Kuperberg 
Emailhttps://perso.ens-lyon.fr/denis.kuperberg/ 
UrlCNRS, ENS Lyon 



Aucun document lié à cet événement.

Retour
Retour à l'index