This program is tentative and subject to change.

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today’s small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. Kontroli is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. Furthermore, Kontroli reduces the checking time using eight threads by up to 6.6x.

Presentation slides (Presentation.pdf)302KiB

This program is tentative and subject to change.

Tue 18 Jan

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

10:20 - 12:00
Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
10:20
25m
Talk
CertiStr: A Certified String SolverDistinguished Paper AwardRemote
CPP
Shuanglong Kan Technische Universität Kaiserslautern, Anthony Widjaja Lin Technische Universität Kaiserslautern and Max-Planck Institute for Software Systems, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern
DOI Pre-print Media Attached
10:45
25m
Talk
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote
CPP
Michael Färber Universität Innsbruck, Austria
DOI Pre-print Media Attached File Attached
11:10
25m
Talk
An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote
CPP
Pre-print Media Attached
11:35
25m
Talk
A Drag-and-Drop Proof TacticRemote
CPP
Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique
DOI Pre-print Media Attached
Hide past events