Links und Funktionen

Sie sind hier: Startseite / Lehre / SS 2013 / Oberseminar / Brigitte Pientka, Beluga^mu: Programming proofs in context


Brigitte Pientka, Beluga^mu: Programming proofs in context

TCS Oberseminar, Mittwoch, 31.07.2013 14:15 Uhr in L109
Wann 14:15 15:15 31.07.2013
von bis
Wo L109
Termin übernehmen vCal

Brigitte Pientka
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.


abgelegt unter: