02.11. Nuria Brede: lambda-mu-PRL - Klassisches Schließen in der konstruktiven Typentheorie
Im Vortrag stelle ich einen Ansatz zur Integration des $\lambda\mu$-Kalküls in die konstruktive Typentheorie des Beweisassistenten Nuprl vor...
| Was |
|
|---|---|
| Wann |
02.11.2010 von 14:15 bis 15:45 |
| Wo | 3.04.1.02 |
| Termin übernehmen |
vCal
iCal
|
Im Vortrag stelle ich einen Ansatz zur Integration des $\lambda\mu$-Kalküls in die konstruktive Typentheorie des Beweisassistenten Nuprl vor.
Die konstruktive Logik des Nuprl- Systems bietet die Möglichkeit, funktionale Programme aus dem Beweis ihrer Spezifikation zu extrahieren. Dieses Prinzip ist als Beweise-als-Programme/Formeln-als-Typen/Curry-Howard-Korrespondenz für konstruktive Logik bekannt.
$\lambda\mu$-Kalküle erweitern dieses Prinzip um Beweisterme für klassische Logik.
Ziel ist nun eine flexiblere Beweisumgebung, die sowohl klassische als auch konstruktive Beweise erlaubt, dabei jedoch anhand des Beweisterms klassische von konstruktiven Beweisen unterscheiden kann.
