Evènement pour le groupe Séminaire Méthodes Formelles

Date 2019-04-30  11:00-12:00
TitreLinearity 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. 
OrateurPierre Clairambault 
UrlCNRS, ENS Lyon 

Aucun document lié à cet événement.

Retour à l'index