  Type theories, logical frameworks and meta-languages form a common foundation
for designing, implementing, and reasoning about formal languages and their
semantics. They are central to the design of modern programming languages,
certified software, and domain specific logics. More generally, they continue
to influence applications in many areas in mathematics, logic and computer
science.
  The Logical Frameworks and Meta-languages: Theory and Practice workshop aims
to bring together designers, implementers, and practitioners working on these
areas, and in particular about: the automation and implementation of the
meta-theory of programming languages and related calculi; the design of proof
assistants, automated theorem provers, and formal digital libraries building
upon logical framework technology; theoretical and practical issues concerning
the encoding of variable binding and fresh name generation, especially the
representation of, and reasoning about, datatypes defined from binding
signatures; case studies of meta-programming, and the mechanization of the
(meta) theory of descriptions of programming languages and other calculi.
  This volume contains the final and revised versions of the papers presented
at LFMTP 2010, which was held on July 14, 2010 in Edinburgh (UK). LFMTP 2010
was part of the Federated Logic Conference (FLoC 2010), and affilated with LICS
2010.
