Programming languages with modules and objects support highly functional systems where applications can snap together components on a custom basis. While functionality can be increased by using small modules, performance overheads and configuration difficulty may be prohibitive. To address these problems, I propose the use of logical programming environments (LPEs) to enable cross-module program transformation and verification. We have demonstrated the effectiveness of this method by carrying out significant systems implementations in a specific LPE called MetaPRL.

The talk will present MetaPRL, a system I developed as part of my thesis research. To the user, MetaPRL behaves as a development assistant, where the programming environment is augmented by a rich logical superstructure that can be called upon, when desired, to perform program transformation and verification.

I'll discuss two applications of this approach to the Ensemble group communication system. One is automatic and verified code optimization, and the other is modular interactive verification of safety properties of protocol stacks.