Thursday 25 March 2021, 15:00, online: Le Framework K, Amélie Ledein (LMF, deducteam).

L'objectif de cette séance de travail Deducteam est de vous présenter le framework K de Grigore Rosu (kframework.org), en se basant sur plusieurs articles et sur la présentation invitée à CPP'2020 (https://popl20.sigplan.org/details/CPP-2020-papers/29/Invited-talk-Matching-Logic-The-Foundation-of-the-K-Framework).

Cet outil est le fruit de 20 ans de recherche et permet de générer un certain nombre d'outils (compilateur, model-checkeur, prouveur automatique, etc.) à partir d'une unique sémantique du langage de programmation considéré.

Après une présentation générale, avec démonstration, du framework K et de ses règles de réécriture, je parlerai également de la logique sous-jacente de K : le matching-logic. Un focus sera également fait sur la génération automatique, à partir d'une sémantique, de prouveurs automatiques.