Certified automated theorem proving for types

Add to your list(s) Download to your calendar using vCal

• Ekaterina Komendantskaya, Heriot-Watt University, Edinburgh
• Friday 20 May 2016, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

Two facts are universally acknowledged:—critical software must be subject to formal verification and—modern verification tools need to scale and become more user-friendly in order to make more impact in industry.

There are two major styles of verification: (1) algorithmic: verification problems are specified in an automated prover, e.g. (constraint) logic programming or SMT solver, and properties of interest are verified by the prover automatically. Such provers can be fast, but their trustworthiness is hard to establish without producing and checking proofs. This is due to complexity of modern-day solvers, e.g. SMT solvers have codebases 100K in C++. These tools exhibit bugs and are not trustworthy enough for critical systems.

An alternative is (2) a typeful approach to verification: instead of verifying programs in an external prover, a programmer may record all properties of interest as types of functions in his programs. Thanks to Curry-Howard isomorphism, type inhabitants also play the role of runnable functions and proof witnesses, thus completing the certification cycle.

At their strongest, types can cover most of the properties of interest to the verification community, e.g. recent dialects Liquid Haskell and F\star allow pre- and post-condition formulation at type level. But, when properties expressed at type level become rich, type inference engines have to assume the role of automated provers, e.g. Liquid Haskell and F\star connect directly to SMT solvers. Thus, once again, we delegate trust without having proper certification of automated proofs.

In this talk, I will tell about our recent work that resolves the above dichotomy “scale versus trust” by offering a new, typeful, approach to automated proving for type inference. Recently, we designed a new method of using logic programming in Haskell type class inference: Horn clauses can be represented as types, and proofs by resolution—as proof terms inhabiting the types. Thus, automated proofs by resolution plug in directly to Haskell’s type system and compiler, while keeping high standards of certification of proofs used in type inference.

Joint work with Peng Fu and Tom Schrijvers, the talk will be based on our FLOPS ’16 paper ``Proof-relevant Corecursive Resolution”.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.