Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 10:00 - 10:30 at Sala XII - Keynote 2 and Research Paper Chair(s): Assia Mahboubi

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract specification of a nondeterministic prover, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

Tue 15 Jan

CPP-2019
09:00 - 10:30: CPP 2019 - Keynote 2 and Research Paper at Sala XII
Chair(s): Assia MahboubiINRIA
CPP-201909:00 - 10:00
Talk
Jasmin BlanchetteVrije Universiteit Amsterdam
DOI
CPP-201910:00 - 10:30
Research paper
Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich
DOI