This dissertation gives an overview of Martin Lof's dependant type theory, focusing on its computational content and addressing a question of possibility of fully canonical and computable semantic presentation.

翻译：本论文概述了马丁-洛夫（Martin Löf）的依赖类型理论，重点探讨其计算内容，并回应了关于实现完全规范且可计算的语义呈现之可能性的问题。