Handcrafted Coq Inversions Made Operational on Operational Semantics
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.
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.
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.