Encoding logical theories of programs

Nowadays, in many critical situations (such as on-board software), it is manda-tory to certify programs and systems, that is, to prove formally that they meet their specifications. To this end, many logics and formal systems have been proposed for rea-soning rigorously on properties of programs and systems. Their usage on non-trivial cases, however, is often cumbersome and error-prone; hence, a computerized proof assistant is required. This thesis is a contribution to the field of computer-aided formal reasoning. In recent years, Logical Frameworks (LF's) have been proposed as general metalan-guages for the description (encoding) of formal systems. LF's streamline the implementa-tion of proof systems on a machine; moreover, they allow for conceptual clarification of the object logics. The encoding methodology of LF's (based on the judgement as types, proofs as λ-terms paradigm) has been successfully applied to many logics; however, the encoding of the many peculiarities presented by formal systems for program logics is problematic. In this thesis we propose a general methodology for adequately encoding formal systems for reasoning on programs. We consider Structured and Natural Operational Semantics, Modal Logics, Dynamic Logics, and the µ-calculus. Each of these systems presents distinc-tive problematic features; in each case, we propose, discuss and prove correct, alternative solutions. In many cases, we introduce new presentations of these systems, in Natural Deduction style, which are suggested by the metalogical analysis induced by the method-ology. At the metalogical level, we generalize and combine the concept of consequence relation by Avron and Aczel, in order to handle schematic and multiple consequences. We focus on a particular Logical Framework, namely the Calculus of Inductive Con-structions, originated by Coquand and Huet, and its implementation, Coq. Our inves-tigation shows that this framework is particularly flexible and suited for reasoning on properties of programs and systems. Our work could serve as a guide and reference to future users of Logical Frameworks.