Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                         VENDREDI 18 janvier, 10h30

                              ---------------
                              Gregory Malecha
                              ---------------

                             Harvard University

                       =============================
                       Reflecting Modular Automation
                       =============================

I describe a method for building composable and extensible
verification procedures within the Coq proof assistant.  Unlike
traditional methods which rely on run-time generation and checking of
proofs, we use verified-correct procedures with Coq soundness
proofs. Though they are internalized in Coq's logic, our provers
support user extensions to enable reasoning over new domains and about
abstract predicates. These extensions can be modularly combined into
reusable "strategies" that can be applied in many contexts. This is
enabled by a rich handling of unification and a formulation of
environments that supports extension. We instantiate the technique to
the verification of imperative programs and show how reflective
tactics can be used to reduce heap implications contains abstract
predicates.

Bio

Gregory Malecha is a graduate student at Harvard co-advised by Greg
Morrisett (Harvard) and Adam Chlipala (MIT). His research interests
lie in the realm of program verification and compilation. With the
former he has been working on Bedrock, a Coq framework for
verification of low-level programs which leverages a combination of
higher-order logic and separation logic. His recent work has focused
on principled, extensible automation in Coq by reflecting general
theorems which can be used by general reflective procedures. He has
also been investigating general progamming in Coq by building a
compiler from Coq to LLVM. The development has followed a
Haskell-style, leveraging monads and type classes to achieve
abstraction. Gregory is an NSF Graduate Research Fellow and a Facebook
Fellow.