Synthèse d'articles et mini projet de programmation

Cours de Programmation par Contraintes

DEA Programmation: "Semantique, Preuves et Langages"
 

Année 2003

Francois Fages

 projet Contraintes

INRIA Rocquencourt



Le cours de Programmation par Contraintes ne comprend pas d'examen écrit mais une évaluation qui se base 

  1. sur la présentation orale (le 31 mars?) d'une synthèse d'articles sur un thème à choisir dans la liste suivante
  2. sur un mini projet de programmation (a remettre avant le 24 mars).

Le mini projet de programmation consiste à écrire un programme (logique avec contraintes) pour résoudre "le problème du golfeur sociable". Nous préconisons l'utilisation de GNU-Prolog (et éventuellement de l'interface graphique CLPGUI) mais l'utilisation de tout autre langage de programmation ou bibliothèque est bienvenue. Bien sûr nous ne demandons pas de résoudre le problème ouvert d'existence d'une solution sur 10 semaines, ni de forcément retrouver la meilleure solution connue de 9 semaines, mais au minimum d'écrire un programme correct.

La synthèse d'article constitue la partie principale de la note pour ce cours. Chaque étudiant choisit un thème et présente en 30 min. à l'aide de transparents une synthèse des articles proposés sur ce thème. Votre exposé devra , sur une base technique, mettre en lumière les points de la démarche étudiée qui vous paraissent importants, et éventuellement réaliser une critique montrant les limites de l'approche. On appréciera particulièrement la prise de recul par rapport aux articles originaux.

Chaque étudiant présente un sujet différent: envoyez votre choix dès que vous vous décidez!
 

Preuves de programmes concurrents avec contraintes : (--> Pierre-Yves Strub)

F. de Boer, M. Gabbrielli, E. Marchiori et C. Palamidessi Proving Concurrent Constraint Programs Correct, TOPLAS 1998.

L'article originel présentant la sémantique dénotationnelle des langages CC est le suivant:
V. Saraswat, M. Rinard et P. Panangaden Semantic Foundations of Concurrent Constraint Programming, POPL 1991.


Langages concurrents avec contraintes et logique linéaire : (--> Alexis Saurin)

 Linear concurrent constraint programming: operational and phase semantics, François Fages, Paul Ruet and Sylvain Soliman. Journal of Information and Computation 165(1) pp.14-41. February 2001.

Phase model checking for some linear logic calculi by Sylvain Soliman. workshop LPAR, Cuba, decembre 2001.

Un article préliminaire sur le sujet est
Higher-order linear concurrent constraint programming. Vijay Saraswat and Pat Lincoln. Draft July 1992. Xerox Parc.



Langages de règles et contraintes :  (-->  Richard Bonichon)

Theory and Practice of Constraint Handling Rules, Special Issue on Constraint Logic Programming (P. Stuckey and K. Marriot, Eds.), Journal of Logic Programming, Vol 37(1-3), October 1998. 

Site  CHR

Site du système CHR


Interprétation abstraite de programmes logiques avec contraintes: (--> Frederic Beal)

M. Hermenegildo,G. Puebla,K. Marriott,P. Stuckey.Incremental Analysis of Constraint Logic Programs (also available in ps). ACM Transactions on Programming Languages and Systems, Vol. 22, Num. 2, pages 187-223, ACM Press, March 2000.


Site du système ciaopp et download.



Typage prescriptif : (--> Mariela Pavlova)

Typed Prolog: A Semantic Reconstruction of the Mycroft-O'Keefe Type System, T.K.Lakshman and U.S. Reddy, in V.Saraswat and K.Ueda (eds) Logic Programming: 1991 International Symposium, MIT Press, 1991, pp. 202-217.
Typing Constraint Logic Programs by François Fages and Emmanuel Coquery. Journal of Theory and Practice of Logic Programming TPLP 1(6)., pp.751-777. November 2001.

Site du système TCLP.


Typage descriptif : (--> Rémi Haemmerlé)

Logic Programs as Types for Logic Programs,  T. Frühwirth, E. Shapiro, M. Vardi and E. Yardeni,
6th Annual IEEE Symposium on Logic in Computer Science (LICS), (G. Kahn, ed.), Amsterdam, July 1991, pp. 300-309,

A Finite Presentation Theorem for Approximating Logic Programs N. Heintze, J. Jaffar POPL'90. 1990.


Machine abstraite de Warren

H. Ait Kaci, Warren's abstract machine, a tutorial reconstruction
Ph. Codognet and D. Diaz Design and implementation of the GNU Prolog system
Contraintes globales: (--> Alexiane Gaudel)
Tutorial on global constraints N. Beldiceanu and M. Carlsson. CP'2002.

Introducing global constraints in CHIP N. Beldiceanu and E. Contejean. Mathematical and Computer Modeling

 A Global Constraint Combining a Sum Constraint and Difference Constraints. Jean-Charles Régin, Michel Rueher:CP 2000: 384-395. Springer-Verlag. LNCS 1894.

A Filtering Algorithm for Constraints of Difference in CSPs. Jean-Charles Régin. AAAI, Vol. 1 1994: 362-367


Symétries : (--> Nicolas Zinovieff)

R. Backofen and S. Will, Excluding symmetries in constraint-based search  In: Constraints: Special Issue on CP2001, 2002

I. Gent, W. Harvey and T. Kelsey, Groups and constraints: symmetry breaking during search. Constriant Programming 2002, Ithaca, USA, September 2002. LNCS 2470, pp. 415-430, Springer Verlag.



Vérification de systèmes à états infinis en programmation logique avec contraintes : (--> Jean-Marc LHOPITAL)

Model Checking in CLP. Giorgio Delzanno & Andreas Podelski . Proc TACAS 99 Springer Verlag.

Verification of Consistency Protocols via Infinite-state Symbolic Model Checking: A Case Study Giorgio Delzanno. FORTE/PSTV 2000, October 2000.

Site du système DMC

Contraintes flexibles:
Semiring-based constraint logic programming: syntax and semantics,
S. Bistarelli, U. Montanari, F. Rossi, ACM TOPLAS, vol. 23, n.1, 2001.

CP 2001 tutorial on soft constraints: models, algorithms, and applications.
Pedro Meseguer, Francesca Rossi, Thomas Schiex.
Transparencies: part 1: models , part 2: algorithms , part 3: applications .

Site du "soft configurator".



Langages concurrents avec contraintes et systèmes biologiques : (--> Jean Krivine)
A. Bockmayr and A. Courtois, Using hybrid concurrent constraint programming to model dynamic biological systems.  18th International Conference on Logic Programming, ICLP'02, Copenhagen, July 2002

N. Chabrier and F. Fages Symbolic model checking of biochemical networks In Computational Methods in Systems Biology, Rivereto, Italy, March 2003.

Site du projet CPBIO