The earliest implementation of this research was done by a student (Roman Ginis) working with the author in 1998. We used the Boyer-Moore theorem prover to hand-specify the above examples (and more) and prove semantic compositionality. Glue code was also written by hand to see what steps were necessary, in typical structured languages, for realizing the resulting interpretations. We have now developed the theoretical infrastructure to completely describe the semantic components and reason about their composition. We also have a realization of the theory in a kind system implemented in SRI’s Maude logical framework. Currently, the realization of renaming, reordering, and simple interpretations is direct: it is snippets of Java program code that are explicit realizations of the corresponding interpretation. In general, Our next step is to “lift” these examples into a general context, automatically generating code in a variety of contexts, rather than just using pre-written, parameterized glue code. To this end, we have developed a distributed component-based web architecture called the Jiki for use as a test-bed of semantic compositionality. The Jiki’s components are distributed JavaBeans, and they interact via a number of technologies including local and remote method calls, message passing via HTTP and other protocols, and a tuple-based coordination mechanism based upon Jini’s JavaSpaces. These components have already been specified with both the Extended BON specification language as well as our semantic properties in their program code.
