Representing Program Logics in Evaluation Logic

We consider the representation of three program logics in ELT (Evaluation Logic): V T LoE (Variable Typed Logic of Effects), modal µ-calculus, Hoare’s Logic. The most interesting result is the definitional extension of ELT with logical operators inspired by V T LoE. Unlike their original counterparts, these logical operators make sense for a wide range of programming languages. In fact, they are defined independently from the interpretation of computational types, and their logical properties are derivable from the axioms of ELT. Also for the modal µ-calculus it is possible to give a treatment in terms of ELT far more general than that in terms of Labelled Transition Systems. We have considered also a representation of Hoare logic into ELT, but we have not achieved results at the same level of generality reached for V T LoE