Dependent Type Theory with Contextual Types

Francisco Ferreira (joint work with David Thibodeau and Brigitte Pientka)

We present Orca, a prototype proof assistant based on type theory with support for Higher Order Abstract Syntax (HOAS) by extending Martin-Löf style type theory with contextual types and a specification framework based on the logical framework LF. This system can be seen as the extension of the theory of Beluga into full dependent types. The prototype is meant to explore both the type theoretic ideas and implementation aspects such as enabling the user to omit mentioning contextual boxes when it is possible to infer their existence.