  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.
