# ITP on Sunday, July 11th

09:00‑10:00 Session 1
Chair: Matt Kaufmann [NOTE: A copy of the full program, with links to slides as well as to the agenda and minutes of the business meeting, may be found HERE.]
Location: AT LT5
 10:30 Ramana Kumar and Michael Norrish (Nominal) Unification by Recursive Descent with Triangular Substitutions We mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including $\alpha$-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success. This style of algorithm has performance benefits and has not been mechanised previously. The algorithms use nested recursion so the termination proofs are non-trivial; the termination relation is also slightly different from usual. 11:00 Jean-François Dufourd and Yves Bertot Formal study of plane Delaunay triangulation This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set. 11:30 Sylvie Boldo, François Clément, Jean-Christophe Filliatre, Micaela Mayero, Guillaume Melquiond and Pierre Weis Formal Proof of a Wave Equation Resolution Scheme: the Method Error Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked. 12:00 Anthony Fox and Magnus Myreen A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. This is a modern RISC architecture with many advanced features. The formalization is detailed and extensive. Considerable tool support has been developed, with the goal of making the model accessible and easy to work with. The model, and supporting tools, are publicly available and we wish to encourage others to make use of this resource. This paper explains our monadic specification approach and gives some details of the endeavours that have been made to ensure that the sizeable model is valid and trustworthy. A novel and efficient testing approach has been developed, based on automated forward proof and communication with ARM development boards.