Séminaires des équipes de recherche
Funlogic: Mixing logic and functional programming styles
- Date : 6/04/2012
- Lieu : Inria - Rocquencourt - Amphithéâtre Alan Turing
- Intervenant(s) : Tim Sheard - Portland State University
- Organisateur(s) : Gallium - Moscova
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.