slepice: Towards a Verified Implementation of Type Theory in Type Theory

摘要

Dependent types have proven a useful technique for development of verified software. Despite the existence of many systems based in dependent type theory, mostly interactive theorem provers but also programming languages, there is no system that would itself be implemented using dependent types. Recently, a new approach to type inference and term synthesis for type theory with dependent types emerged that separates the process into an analysis phase that is carried out in type theory, and a search phase that is carried out in a logic programming engine. We describe an architecture of type inference and term synthesis engine for a language with dependent types that is based on the new approach and that is feasible to implement using a dependently typed language. We demonstrate the architecture by describing slepice, its particular implementation.