Séminaire Cambium, Inria Paris
                                 Amphi Lions
                           Vendredi 14 mars, 10h30

                            Mathis Bouverot-Dupuis
                                 Inria Paris

                     Code Generation via Meta-programming
                    in Dependently Typed Proof Assistants

Dependently typed proof assistants offer powerful meta-programming
features, which users can take advantage of to implement proof
automation or compile-time code generation. We survey meta-programming
frameworks in Rocq, Agda, and Lean, with seven implementations of a
running example: deriving instances for the Functor type class. This
example is fairly simple, but sufficiently realistic to highlight
recurring difficulties with meta-programming: conceptual limitations
of frameworks such as term representation – and in particular binder
representation –, meta-language expressiveness, and verifiability as
well as practical limitations such as API completeness, learning
curve, and prover state management. We conclude with insights
regarding features an ideal meta-programming framework should provide.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.