Room 206 (2nd floor, badged access)
19 June 2024 - 09h30
Recent advances on the Braga method
by Jean-François MONIN from Verimag, Polytech Grenoble.
Abstract: The Braga method, designed by D. Larchey-Wendling and J-F. Monin, allows us to define in Coq recursive programs without a priori knowledge on their termination domain, to be be extracted as expected in, say, OCaml. More precisely, it is enough to know in advance *how* termination is ensured, but not *why*, and this how is syntactically derived from the intended code to be extracted. In particular, it makes it possible to extract meaningful programs, such as DFS, that don't always terminate and to formally reason about them. Then the why can be considered separately -- total correctness can be studied on the same footing as partial correcness properties.
Given a program Pgm to be derived, the method is based on:
- an inductive definition of the input-ouput relation G (for graph) which can be seen as a syntactical specification of Pgm;
- a corresponding inductive definition of D, the domain of G;
- suitable projections for recovering subterms of a term of type D.
The talk will quickly recall former work sketched in ConstructiveEpsilon and in the Coq'Art, then focus on some pros and cons regarding G:
- is it better to work directly with D, without G? dependent small inversions [TYPES'22] are part of the answer;
- do we have the choice? Clearly no, when G is used in the definition of D, in particular in the presence of embedded recursion. However we recently discovered with Pierre Corbineau that the situation is more open than appears at first sight.
Séminaire dans le cadre de la visite de M. Sozeau et Y. Forster à Verimag.
