Automatic generation of proof terms in dependently typed programming languages

Franck Slama. Automatic generation of proof terms in dependently typed programming languages. PhD thesis, University of St Andrews, UK, 2018. [doi]

Abstract

Abstract is missing.