Dependently Typed Programming with Domain-Specific Logics

We define a dependent programming language in which programmers can define and compute with 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 compiletime. In previous work, we studied a simply-typed framework for representing and computing with variable binding [LICS 2008]. 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.