Brigitte Pientka, Beluga^mu: Programming proofs in context
Beluga^mu: Programming proofs in context
We extend a general purpose functional language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. This allows programmers to specify formal systems and proofs within the logical framework LF using higher-order abstract syntax and avoids common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. In addition, programmers, can index ML types with contexts and contextual LF objects allowing users to define relations between them. This leads to a powerful language, Beluga^mu which supports manipulating and analyzing contexts and contextual LF objects. To illustrate the elegance and effectiveness of our language, we give concise programs for closure conversion and weak normalization.