
Evènement pour le groupe Séminaire Méthodes Formelles
Date  20190430 11:0012:00 
Titre  Linearity in HigherOrder Recursion Schemes 
Résumé  HigherOrder ModelChecking (HOMC) has recently emerged as an approach
to automated verification of higherorder programs, prompted by Ong's
2006 result that Monadic Second Order Logic (MSO) is decidable on
infinite trees generated by HigherOrder Recursion Schemes (HORS).
Implementations report encouraging results despite an awful theoretical
worst case complexity.
In principle, HOMC algorithms work by reduction to Ong's theorem. In
practice, this often involves CPS translations which are costly in terms
of complexity, and so as to get tight complexity people have instead
reproved variations of Ong's theorem for extensions of HORS (with data,
or callbyvalue) and drastically restricted fragments of MSO.
In this talk, I will introduce Linear HORS (LHORS), an extension of HORS
with additional type constructors imported from Linear Logic. Data and
callbyvalue evaluation admit a finer translation to LHORS exploiting
the idea of linearlyused continuations. Moreover LHORS enjoy a
decidable modelchecking problem, whose complexity essentially ignores
linear types. In this way we recover and extend several developments
that were originally proved independently of Ong's theorem.
This is joint work with Andrzej Murawski and Charles Grellois, presented
at POPL'18. 
Lieu  178 
Orateur  Pierre Clairambault 
Email  http://perso.enslyon.fr/pierre.clairambault/ 
Url  CNRS, ENS Lyon 
Aucun document lié à cet événement. RetourRetour à l'index
 