POPL 2019 (series) / CPP 2019 (series) / CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 14-15 2019 /
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first-order resolution prover, an imperative SAT solver, and generalized term or- ders for λ-free higher-order logic.
Tue 15 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Tue 15 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00 Talk | Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL CPP Jasmin BlanchetteVrije Universiteit Amsterdam DOI | ||
10:00 - 10:30 Research paper | A Verified Prover Based on Ordered Resolution CPP Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich DOI |