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 6 avril, 10h30

                                 ----------
                                 Tim Sheard
                                 ----------

                         Portland State University

               ==============================================
                                 Funlogic:
               Mixing logic and functional programming styles
               ==============================================

We have been designing a language in which programmers can use both the logic
and functional styles.

  1) In the functional style, programmers introduce variables and assign the
     variables values by describing a computation that evaluates to the answer
     desired.

  2) In our language one can also introduce variables by describing what
     properties the variable's values should have using first order logic. The
     language implementation automatically searches for solutions. We call
     these existential declarations.

The language lets the programmer mix computation-based programs with
search-based programs in a completely transparent manner. Existential
variables are bound to conforming values by decision procedures (e.g SAT
solvers, SMT solvers, the Simplex algorithm, and Narrowing). Funlogic embeds
multiple external decision procedures using a common framework. Design
principles for embedding decision procedures are developed and illustrated for
three different decision procedures from widely varying domains.