We define a dependent programming language in which programmers can define and
compute with \emph{domain-specific logics}, such as an access-control logic that
statically prevents unauthorized access to controlled resources.  Our language
permits programmers to define logics using the LF logical framework, whose
notion of binding and scope facilitates the representation of the consequence
relation of a logic, and to compute with logics by writing functional programs
over LF terms.  These functional programs can be used to compute values at
run-time, and also to compute types at compile-time.  In previous work, we
studied a simply-typed framework for representing and computing with variable
binding.  In this paper, we generalize our previous type theory to account for
dependently typed inference rules, which are necessary to adequately represent
domain-specific logics, and we present examples of using our type theory for
certified software and mechanized metatheory.