Evènement pour le groupe Séminaire Méthodes Formelles
|Date|| 2019-04-30 11:00-12:00|
|Titre||Linearity in Higher-Order Recursion Schemes |
|Résumé||Higher-Order Model-Checking (HOMC) has recently emerged as an approach
to automated verification of higher-order programs, prompted by Ong's
2006 result that Monadic Second Order Logic (MSO) is decidable on
infinite trees generated by Higher-Order 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 call-by-value) 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
call-by-value evaluation admit a finer translation to LHORS exploiting
the idea of linearly-used continuations. Moreover LHORS enjoy a
decidable model-checking 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. |
|Orateur||Pierre Clairambault |
|Url||CNRS, ENS Lyon |
Aucun document lié à cet événement.RetourRetour à l'index