Write a Blog >>
Thu 22 Nov 2018 16:05 - 16:30 at Boothzaal - 3 Chair(s): Robbert Krebbers

First-order theorem provers based on superposition, such as E, SPASS, and Vampire, play an important role in formal software verification. They are based on sophisticated logical calculi that combine ordered resolution and equality reasoning. They also employ advanced algorithms, data structures, and heuristics.

As a step towards verifying the correctness of state-of-the-art provers, we specify, using the Isabelle/HOL proof assistant, a purely functional ordered resolution prover and formally 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.

(See http://matryoshka.gforge.inria.fr/pubs/fun_rp_paper.pdf for details.)

Thu 22 Nov
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:40 - 17:20: 3PLNL at Boothzaal
Chair(s): Robbert KrebbersDelft University of Technology
15:40 - 16:05
Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel, Belgium
16:05 - 16:30
A Verified Automatic Prover Based on Ordered Resolution
Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich
16:30 - 16:55
Type Systems with Constraints for ML Type Inference with the Implementation in Haskell
Alen ArslanagićUniversity of Groningen
16:55 - 17:20
Improving pattern matching style
Alejandro SerranoUtrecht University, Netherlands