Strategies for Interactive Proof and Program Development in
Martin-L\"of Type Theory (Extended abstract)

Marcin Benke
G\"oteborg, Sweden

Abstract

We propose some strategies for automatic tools facilitating
interactive proof and program development in the proof editor Alfa
based on Martin-L\"of Type Theory.