Dependently Typed Programming with Domain-Specific Logics

摘要

This dissertation describes progress on programming with domain- specific specification logics in dependently typed programming languages. Domain-specific logics are a promising way to verify software, using a logic tailored to a style of programming or an application domain. First goal of the research is to show that it is possible to define, study, automate, and use domain-specific logics within a dependently typed programming language. We demonstrate this with an example showing how to embed a security-typed language using dependent types. This suggests that better support for programming with logics in type theory will facilitate this style of program verification. The central notion in logic is consequence - entailment from premises to conclusions - and two notions of consequence are necessary for programming with logics: derivability, which captures uniform reasoning, and admissibility, which captures inductive proofs and functional programs. Presently, derivability is better supported in LF-based proof assistants such as Twelf, Delphin, and Beluga, whereas admissibility is better supported in proof assistants based on Martin-Loef type theory. Second contribution is to show that it is possible to implement, within a dependently typed programming language, a logical framework that allows derivability and admissibility to be mixed in novel and interesting ways. The framework is simply-typed, suitable for programming with abstract syntax but not logical derivations. Third contribution is to generalize this framework to dependent types We describe Directed Type Theory (DTT), a dependent type theory, which equips each type with a notion of transformation on its elements. The structural properties of a logic arise as a special case, considering a type of contexts equipped with an appropriate notion of transformation. DTT generalizes recent connections between type theory, homotopy theory, and category theory to the asymmetric case.