Developing a Modal Specification Language
Meta-logical frameworks are used to create and analyze formal specifications of programming languages. This research builds upon McDowell and Miller's meta-logical framework FOƛ ∆N. FOƛ ∆N separates the meta-logic used for reasoning from the specification language in which the programming language is encoded. This separation adds a level of indirection that can make the specification cumbersome. The modal meta-logic we designed avoids this indirection by making the specification language a subset of the meta-logic, using a modal operator to distinguish the specification from statements about the specification. We prove that our logic's specification language subset is equivalent to first-order logic, the specification language used in FOƛ ∆N.