Axe : SciLex
Sujet : Scilex-3 From high-level to low-level certification
Directrice de thèse: Catherine Dubois
Doctorante : Amélie Ledein
Co-encadrant : Valentin Blot
Laboratoire gestionnaire : Inria SIF
Autres partenaires : LSV, SAMOVAR
Début : octobre 2020
Productions scientifiques :
Ressources :
Contexte :
K is a semantical framework for formally describing the semantics of programming languages. It is also an environment that offers various tools to help programming with the languages specified in the formalism. It is for example possible to execute programs and to check some properties on them, using the KProver tool.
Dedukti is a logical framework allowing the interoperability of proofs between different formal proof tools. It is based on the λΠ-calculus modulo theory, an extension of the type theory by adding rewriting rules in the conversion relation. The flexibility of this logical framework allows to encode many theories like 1st order logic or simple type theory.
Thanks to the logical framework Dedukti, the objective of this thesis is to verify formal proofs about the semantics of programming languages, described in the semantical framework K, and to reuse of such proofs in different proof tools.