Newsgroups: fr.announce.seminaires Distribution: fr To: fr-sem@frmug.org From: Didier.Remy@inria.COUPER-CECI.fr Organization: INRIA-Rocquencourt Subject: SEM - INRIA : Cristal - 26/05/00 - Paris - FR *** Rectificatif: attention à l'horaire inhabituel *** http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ . / _ _ / ___ __ /_ _ / /| /| _ __ __ _ _ / / \ / \ _ / / / /_ / __| / _ / |/ | / \ /_ / / \ | / __| |___ |_/ |_/ |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ / / I N R I A - Rocquencourt, Salle de conference du Bat 11 Vendredi 26 mai, 14h ------------------- Richard B. Kieburtz ------------------- Oregon Graduate Institute and INRIA-Rocquencourt ====================== A Logic for Strategies ====================== Source-to-source transformations of functional language programs have long been studied and many transformations are applied automatically in state-of-the-art compilers. However, it is difficult, even for the compiler implementors, to say exactly which transformation schemes are effective on a given program. Stratego is a language designed by Eelco Visser to support programming of strategies for the automatic transformation of terms. Stratego provides a well-defined operational semantics for transformation strategies. However, even this degree of formalization does not meet the need for a logical characterization of properties of terms before and after transformation. In this talk, I propose that Computational Tree Logic (CTL) is an appropriate framework in which to express properties of term structures. With CTL as a modal logic of terms, we begin to develop a weakest-precondition logic of proof rules for strategies. The approach is illustrated with proof rules for many of the strategy constructions of Stratego.