Axe : SciLex
Sujet : Scilex-3 From high-level to low-level certification
Directeurs de thèse : Frédéric Blanqui
Co-directrice de thèse: Catherine Dubois
Laboratoire gestionnaire : Inria SIF
Autres partenaires : LSV, SAMOVAR
Doctorante : Amélie Ledein
Début : 2020
Productions scientifiques :
Ressources :
Contexte : Lambdapi is an interactive front-end for Dedukti, a proof checker for a logical framework called the λΠ-calculus modulo rewriting, which is an extension of the simply-typed λ-calculus (the basis of functional programming languages like OCaml and Haskell) with dependent types (e.g. vectors and matrices of arbitrary dimensions) and an equivalence relation on types generated by user-defined rewrite rules.
Thanks to rewriting, Dedukti allows the formalization of proofs that cannot be done in other proof assistants.
However, there is currently no user support for doing inductive definitions and proofs in Dedukti. The goal of this project is therefore to design and develop a tool for automatically generating induction principles for large or complex induction definitions, and apply this tool to the formalization and translation of processor instruction sets and their semantics used in the industry (ARM, Intel, etc.) which are examples of inductive definitions with hundreds of cases.