La journée FAC'93 a eu lieu le mardi 20 avril 1993, salle de Conférence du LAAS.

Programme de la journée :

• Les réseaux naturels. Pierre Azéma (LAAS-CNRS)

  Un réseau de Petri, condition-événement, construit une preuve. Il dénote donc un programme. Cette assertion est expliquée au moyen de l’illustration par des réseaux du livre de Girard, preuves et types. Il s’agit de comparer les assertions suivantes: des préconditions, une transition, des postconditions forment un réseau. Des hypothèses, une déduction, des conclusions forment une preuve. Des types, un constructeur, de nouveaux types forment un calcul. Des agents, un échange, de nouveaux agents forment un système de communication.

• Formalisation des objets concurrents. Jean-Paul Bahsoun, Corinne Servières (IRIT-UPS)

  Nous développons un système de preuve formel pour représenter et valider des concepts orientés objet dans un environnement parallèle. Deux problèmes sont étudiés : le premier concerne la composition d’un objet à partir d’autres objets plus simples , dans un environnement parallèle. Le second est celui de trouver des solutions formelles pour traiter l’interférence entre l’héritage et le parallélisme. Ces deux problèmes ont fait l’objet d’application pour les logiques non classiques comme la logique temporelle et la logique dynamique. Notre étude s’étendra vers la définition d’une nouvelle logique pour traiter ces problèmes d’une façon naturelle.

• Le projet LCS. Etat et perspectives. Bernard Berthomieu (LAAS-CNRS)

  Le langage LCS étend le langage fonctionnel Standard ML par des comportements qui permettent l’expression de programmes parallèles et communicants, et depuis lesquels peuvent être créés des processus. Le langage des comportements est basé sur une extension d’ordre supérieur du formalisme des processus communicants (CCS) de Robin Milner. Une extension non triviale du mécanisme de typage polymorphe de Standard ML permet d’inférer des types pour les comportements, le type d’un comportement associant un type polymorphe à chaque label de communication. Une technique d’exécution est définie pour les processus, conforme à la sémantique opératoire des agents CCS, et préservant les règles d’évaluation de Standard ML.

• PERF : un environnement de raisonnement formel. Pierre Michel, Jacques Cazin (DERI-CERT)

  PERF «Prototype d’Environnement de Raisonnement Formel» est basé sur le lambda-calcul typé «Logical Framework d’Edimbourg» qui permet d’encoder des logiques et de faire des vérifications de preuves par simples contrôles de types (cf. l’analogie de CurryHoward : «propositions as types»). PERF propose d’étendre le calcul LF par des facilités pour l’encodage des logiques (abréviations) et par une assistance à la construction de preuves. PERF a été utilisé dans des développements de logiciels basés sur l’approche transformationnelle, pour le passage de spécifications LOTOS à des programmes Ada, et pour vérifier des propriétés de programmes : contrôle de précision, propriétés de sécurité, propriétés des systèmes concurrents.