Definition and Basic Properties of the
Deva Meta-Calculus, Matthias Weber · 1993
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.