BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Certified automated theorem proving for types - Ekaterina Komendan
 tskaya\, Heriot-Watt University\, Edinburgh
DTSTART:20160520T130000Z
DTEND:20160520T140000Z
UID:TALK65216@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Two facts are universally acknowledged: -- critical software m
 ust be subject to formal verification and -- modern verification tools nee
 d to scale and become more user-friendly in order to make more impact in i
 ndustry.\n\nThere are two major styles of verification:  \n(1) algorithmic
 :  verification problems are specified in an automated prover\, e.g.  (con
 straint) logic programming or SMT solver\, and properties of interest are 
 verified by the prover automatically.\nSuch provers can be  fast\, but the
 ir trustworthiness is hard to establish without producing and checking pro
 ofs. This is due to complexity of modern-day solvers\, e.g. SMT solvers ha
 ve codebases 100K in C++. These tools exhibit bugs and are not trustworthy
  enough for critical systems.\n\nAn alternative is (2) a typeful approach 
 to verification: instead of verifying programs in an external prover\, a p
 rogrammer may record all properties of interest as types of functions in h
 is programs. Thanks to Curry-Howard isomorphism\, type inhabitants also pl
 ay the role of runnable functions and proof witnesses\, thus completing th
 e certification cycle.\n\nAt their strongest\, types can cover most of the
  properties of interest to the verification community\, e.g. recent dialec
 ts 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.\n\nIn 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 -- a
 s proof terms inhabiting the types. Thus\, automated proofs by resolution 
 plug in directly to Haskell’s type system and compiler\, while keeping h
 igh standards of certification of proofs used in type inference. \n\nJoint
  work with Peng Fu and Tom Schrijvers\, the talk will be based on our FLOP
 S’16  paper ``Proof-relevant Corecursive Resolution”.
LOCATION:FW26
END:VEVENT
END:VCALENDAR