Room 206 et BBB (code d'accès 506793)
10 June 2021 - 15h00
[FormalProofs] Small inversions and unleashed recursion in Coq, the Braga method
by Jean-François Monin from Verimag
Abstract: How to reason in Coq on recursive functions whose termination is unclear in advance? Including function which are obviously partial, with a complex or even unknown domain of definition? How to write them in the form of Coq functions which on extraction give exactly the expected OCaml program?
The Braga method, originally presented by D. Larchey-Wendling and the speaker in Braga (Types'18) responds positively to these questions. The talk focuses on a key ingredient: the recovery of a structurally decreasing component into a dependent inductive type, written clearly and legibly.
For this it was necessary to develop the technique of small inversion which had been introduced to perform intensive reasoning based on an operational semantics of CompCert and, even to this day, manages situations beyond the reach of the Coq standard tactics.
Pour toutes infos supplémentaires contacter directement Jean-François Monin.
