Tue 17 Jan 2023 11:00 - 11:22 at Studio 1 - Practical Proving Chair(s): Dmitriy Traytel

Proofs automatically generated from proof assistants or automated theorem provers are often several orders of magnitude larger than proofs written by hand. This implies significant challenges for processing such proofs efficiently. It turns out that the data structures to encode terms have a high impact on performance. This article proposes several term data structures; in particular, heterogeneous terms for proof checking that distinguish long- and short-lived terms, and abstract terms for proof parsing. Both term data structures are implemented in the proof checker Kontroli, enabling it to parse and check proofs both sequentially and concurrently without overhead. The evaluation on three datasets exported from proof assistants shows that the new term data structures significantly improve proof checking performance.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Practical ProvingCPP at Studio 1
Chair(s): Dmitriy Traytel University of Copenhagen
11:00
22m
Talk
Terms for Efficient Proof Checking and ParsingRecorded Presentation
CPP
Michael Färber Universität Innsbruck, Austria
11:22
22m
Talk
Compositional pre-processing for automated reasoning in dependent type theoryremote presentation
CPP
Valentin Blot LMF, Inria, Université Paris-Saclay, Denis Cousineau Mitsubishi Electric R&D Centre Europe, Enzo Crance Mitsubishi Electric R&D Centre Europe, Louise Dubois de Prisque LMF, Inria, Université Paris-Saclay, Chantal Keller LRI, Université Paris-Sud, Assia Mahboubi INRIA, Pierre Vial Inria
11:45
22m
Talk
Practical and sound equality tests, automatically
CPP
Benjamin Gregoire INRIA, Jean-Christophe Léchenet Université Côte d’Azur, Inria, Enrico Tassi INRIA
12:07
22m
Talk
Compiling higher-order specifications to SMT solvers: how to deal with rejection constructivelyremote presentation
CPP
Matthew L. Daggitt Heriott-Watt University, Robert Atkey University of Strathclyde, Wen Kokke University of Strathclyde, Ekaterina Komandantskaya Heriot-Watt University, UK, Luca Arnaboldi The University of Edinburgh