| Programming + Verification = Progification (Draft) (2008) | |||||||||||||||
Abstract | |||||||||||||||
| We discuss the rôle Type Theory should play in the formal development of correct programs. We view verification as a programming problem in a sophisticated programming language and evaluate this approach by presenting a number of examples developed in the ALF system. Thereby we exploit the recent advantages in the presentation of Type Theory in particular by using pattern matching as proposed in [Coq92]. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||