LAUSR

This special issue contains extended versions of selected contributions of the eighth International Conference on Interactive Theorem Proving (ITP 2017). The conference was held in Brasília, Brazil, on September 2017 and its proceedings appeared as volume 10499 of the series Lecture Notes in Computer Science (LNCS), published by Springer Nature. The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The papers were carefully reviewed by specialists, including members of the ITP 2017 PCs and additional experts. The reviewers guaranteed both significant additional contributions with respect to the LNCS proceedings and assured the quality standards of the Journal of Automated Reasoning, for which the guest editors are grateful. In the following, a short introduction is given to each of the nine papers included in this volume. InAFormalization of Convex Polyhedra Based on the SimplexMethod, XavierAllamigeon andRicardoD.Katz present a formalization inCoqof the theoryof convexpolyhedra using the MathComp library. The authors use a complete formalization of the simplexmethod, together with the proof of its correctness and termination. This formalization provides an effective way to determine the feasibility of a polyhedral region, and in the case of optimization, the minimum value or a proof of the unboundedness of the objective function. The formal development includes important results such as the duality theorem, Farkas’ lemma, and Minkovski separation theorem. The paper by Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow, A Formal Proof of the Expressiveness of Deep Learning, presents a formalization in Isabelle/HOL of a recent mathematical result, formulated by Cohen et al. This result concerns the higher expressiveness of deep learning over shallow learning for one specific architecture called convolutional arithmetic circuits (CAC). Cohen et al. result states that CAC shallower networks must be exponentially larger than deeper networks expressing the same function. A