InDepTh - Definitions and proofs by induction in dependent type theory 

Axe & tâche scientifique DigiCosme : SciLex
Coordinateurs : Frédéric Blanqui, Inria Saclay - Catherine Dubois, SAMOVAR
Nom & Prénom du Candidat : Amélie Leiden
Adresse mail :
Laboratoire gestionnaire: Inria Saclay
Adossé à l'action DigiCosme : GT UPSCaLe
Durée & Dates de la mission : 3 ans - Octobre 2020 à septembre 2023

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.

Productions Scientifiques :