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.