Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 13:22 - 13:45 at Stifel Theatre - Proof Techniques and Mechanization Chair(s): Niki Vazou

Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning. Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to break the goal into subgoals until all subgoals have been solved. Additionally, it provides support for tactic programming via OCaml and Ltac, so that users can roll their own custom proof automation routines.

Unfortunately, though, these tactic languages share a significant weakness. They do not offer the tactic programmer any static guarantees about the soundness of their custom tactics, making large tactic developments difficult to maintain. To address this limitation, Ziliani et al. previously proposed Mtac, a new typed approach to custom proof automation in Coq which provides the static guarantees that OCaml and Ltac are missing. However, despite its name, Mtac is really more of a metaprogramming language than it is a full-blown tactic language: it misses an essential feature of tactic programming, namely the ability to directly manipulate Coq’s proof state and perform backward reasoning on it.

In this paper, we present Mtac2, a next-generation version of Mtac that combines its support for typed metaprogramming with additional support for the programming of backward-reasoning tactics in the style of Ltac. In so doing, Mtac2 introduces a novel feature in tactic programming languages—what we call typed backward reasoning. With this feature, Mtac2 is capable of statically ruling out several classes of errors that would otherwise remain undetected at tactic definition time. We demonstrate the utility of Mtac2’s typed tactics by porting several tactics from a large Coq development, the Iris Proof Mode, from Ltac to Mtac2.

Tue 25 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30
Proof Techniques and MechanizationResearch Papers at Stifel Theatre
Chair(s): Niki Vazou University of Maryland, USA
13:00
22m
Talk
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Research Papers
Robbert Krebbers Delft University of Technology, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Ralf Jung MPI-SWS, Joseph Tassarotti Carnegie Mellon University, Jan-Oliver Kaiser MPI-SWS, Amin Timany imec-Distrinet KU-Leuven, Arthur Charguéraud Inria, Derek Dreyer MPI-SWS
DOI
13:22
22m
Talk
Mtac2: Typed Tactics for Backward Reasoning in Coq
Research Papers
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET, Robbert Krebbers Delft University of Technology, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek Dreyer MPI-SWS
DOI
13:45
22m
Talk
Compositional Soundness Proofs of Abstract Interpreters
Research Papers
Sven Keidel Delft University of Technology, Netherlands, Casper Bach Poulsen Delft University of Technology, Sebastian Erdweg Delft University of Technology, Netherlands
DOI
14:07
22m
Talk
Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper
Research Papers
Nicolas Tabareau Inria, Éric Tanter University of Chile & Inria Paris, Matthieu Sozeau Inria
DOI