We define a dependently typed 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 a rich logical framework with two function spaces:
representational functions provide a notion of binding and scope
suitable for representing the consequence relation of a logic, whereas
computational functions permit functional programs over such
higher-order representations. In previous work, we studied a
simply-typed framework for representing and computing with variable
binding, organized around the logical principles of polarity and
focusing [LICS 2008]. In the present work, we enrich this framework
with dependency on purely positive data, which yields a language of
types precise enough to adequately represent the judgements of logical
systems.