Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2010/11 / Oberseminar / Brigitte Pientka, Beluga: Programming proofs with contexts and ...


Brigitte Pientka, Beluga: Programming proofs with contexts and ...

TCS Oberseminar, 05.11.2010, 14:15
Wann 14:15 15:15 05.11.2010
von bis
Wo L109
Termin übernehmen vCal

Brigitte Pientka (McGill, Montreal, Canada) 


Beluga: Programming proofs with contexts and ...


Beluga is an environment for programming and reasoning about formal

systems given by axioms and inference rules. It implements the

logical framework LF for specifying and prototyping formal systems

via higher-order abstract syntax. It also supports reasoning: the

user implements inductive proofs about formal systems as dependently

typed recursive functions.  A distinctive feature of Beluga is that

it not only represents binders using higher-order abstract syntax,

but directly supports reasoning with contexts.  Taken together these

features lead to a powerful language which supports writing compact

and elegant proofs.


In this talk, I will discuss the main design ideas and principle of

Beluga by showing the implementation of the type uniqueness proof for

the simply typed lambda-calculus. Using this example, I will contrast

the approach in Beluga to other systems and outline some of our

current and future developments.


abgelegt unter: