  Formal deductive systems are very common in computer science. They are used
to represent logics, programming languages, and security systems. Moreover,
writing programs that manipulate them and that reason about them is important
and common. Consider proof assistants, language interpreters, compilers and
other software that process input described by formal systems. This thesis
shows that contextual types can be used to build tools for convenient
implementation and reasoning about deductive systems with binders. We discuss
three aspects of this: the reconstruction of implicit parameters that makes
writing proofs and programs with dependent types easier, the addition of
contextual objects to an existing programming language that make implementing
formal systems with binders easier, and finally, we explore the idea of
embedding the logical framework LF using contextual types in fully dependently
typed theory. These are three aspects of the same message: programming using
the right abstraction allows us to solve deeper problems with less effort. In
this sense we want: easier to write programs and proofs (with implicit
parameters), languages that support binders (by embedding a syntactic framework
using contextual types), and the power of the logical framework LF with the
expressivity of dependent types.
