Definition and basic properties of the deva meta-calculus

This article presents the definition and some basic properties of the Deva meta-calculus, a generic logical framework whose design was driven by the needs arising from the instantiation to software development methods. As a result, Deva contains structures that do not occur in comparable logical frameworks. There now exist a number of case studies about the formalization of software development methods in Deva. In this article, a structured definition of Deva is presented and basic parts of its language theory, viz Church-Rosser, closure, and strong normalization, are summarized.Major parts of the work reported here were carried out while the author was under contract at the German National Research Centre (GMD) in Karlsruhe and at the University of Karlsruhe