LIFC - A Mechanized Calculus for Aspect-oriented Programming

TitreA Mechanized Calculus for Aspect-oriented Programming
RésuméAspect-oriented programming promises adaptivity: insertion of suitable code fragments at specified points in a program enables systematic tailoring. While introducing flexibility into software production, there are new risks. In current aspect-oriented languages, e.g. AspectJ, aspects can make correct programs fail. In order to offer safe aspects, we endeavor into the verification of the aspect-oriented language paradigm. We construct a base calculus for aspects and mechanize it in the interactive theorem prover Isabelle/HOL. Our aspect calculus is based on the well known Theory of Objects and features a type system for static analysis for which we proved type safety completely in Isabelle/HOL.
Date2008-05-05
Heure14:00
IntervenantKammuler Florian
Page Web
LaboratoireN/A
EtablissementN/A
LieuSalle 404C

Annuaire