We present and discuss various formal]zations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hubert- and Natural Deductionstyle proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed A-calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO. © 1998 Kluwer Academic Publishers.