# Thèse

# 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 :**