Global computing involves the interplay of a vast variety oflanguages, but practially useful foundations for languagespecification and prototyping at the semantic level are lacking.In this talk we present a systematic approach consisting of threetechniques: 1. A generic calculus of explicit substitutions with names (calledCINNI) that allows us give a first-order representation of syntax touniformly deal with all binding aspects.2. An executable representation of Felleisen-style operationalsemantics in terms of first-order rewrite rules.3. A logical framework, namely rewriting logic, that allows us toexpress (1) and (2) and, in addition, language aspects such asconcurrency and non-determinism.We illustrate the use of these techniques in two applications:1. A formal specification and analysis of PLAN, a Packet Language forActive Networks, that has been developed in the Switchware project atUPenn. This work was conducted in the scope of the DARPA ActiveNetwork Program.2. The development of CIAO, a Calculus of Imperative Active Objects, acore language for concurrent object-oriented programming. It isespecially designed to allow a the representation of practicallyrelevant sublanguages of common object-oriented languages such as Java, C#, and C++. This second application is subject of ongoing work.
展开▼
