Title: Handcrafted Coq Inversions Made Operational on Operational Semantics

Speaker: Jean-Francois Monin

　　    VERIMAG, Univ. Joseph Fourier, Grenoble, France

　　    www-verimag.imag.fr/~monin/

Time: 14:00, 20th March 2014

Venue: ROOM 337, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

When reasoning on formulas involving large-size inductively defined relations, such as the semantics of a real programming language, many steps require inversions of hypotheses. The built-in "inversion" Coq tactic can then be used, but it suffers from severe issues of controllability, maintenance and efficiency. This tactic is unusable in practice for large applications.

To circumvent that issue, we propose a proof technique based on the combination of an antidiagonal argument and the impredicative encoding of inductive data-structures. We can then encode suitable helper tactics in LTac, yielding shorter scripts, furthermore more robust against version updates in the background software. We illustrated it within correctness proofs of C programs according to the operational semantics of C defined in Leroy's CompCert project.

Bio:

Jean-Francois Monin worked at France Telecom R&D in applications of Formal Proofs to industrial software. He has been professor at Univ. Joseph Fourier, Grenoble, since 2003. He worked at LIAMA & Tsinghua University from 2009 to 2013.