Newsgroups: fr.announce.seminaires Distribution: fr To: fr-sem@frmug.org From: Didier.Remy@inria.COUPER-CECI.fr Organization: INRIA-Rocquencourt Subject: SEM - INRIA : Para - 10/9/99 - Paris - FR 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 10 septembre, 10h30 ---------- John Field ---------- IBM T.J. Watson Research Center =================================================================== Equations as a Uniform Framework for Operational Semantics, Partial Evaluation, and Abstract Interpretation =================================================================== A variety of disparate methods have traditionally been used to define the operational semantics of languages, to describe partial evaluation, to formalize program analysis as abstract interpretation, and to implement each of these operations in practical systems. In this talk, I argue that _equational logic_ can serve to unify each of these aspects of language manipulation. The benefits of such a unified view are considerable: - Specification of interpreters, partial evaluators, or analyzers can often be done in a _modular_ fashion, simply by adding or removing sets of equations - Equational semantics is very well understood. - Equational systems are particularly amenable to efficient mechanical implementation. I illustrate the relation between equational reasoning, operational semantics, and partial evaluation using a logic for imperative languages called PIM. I then sketch preliminary work on a new approach for systematically developing abstract interpretations from concrete equational specifications. These ideas are illustrated using a "classical" program analysis problem. While this problem would traditionally require three staged analyses, our approach combines these stages in a single fixpoint computation. (Parts of this work are joint with J. Heering, T.B. Dinesh, and J. Bergstra)