Wprowadzenie do systemu Twelf (mini-wykład i pracownia)
Instytut Informatyki UWr
Semestr zimowy 2009/10
Opis przedmiotu
Przedmiot stanowi wprowadzenie do
zagadnień związanych z formalizacją metateorii
języków programowania w systemie
Twelf.
Literatura
- Strona domowa Twelfa
- F. Pfenning, Computation and Deduction
(rozdziały 3 i 5, a być może również 4)
- R. Harper, F. Honsell, and G. Plotkin,
A Framework for Defining Logics
- R. Harper, D. Licata,
Mechanizing Metatheory in a Logical Framework
Czas i miejsce (od 27.11.2009 do 18.12.2009)
- Wykład: piątek 10:15-12:00, sala 325
- Ćwiczenia: piątek 12:15-14:00, pracownia 137
- Konsultacje: czwartek 15:00-17:00, pokój 327
|
Rozkład jazdy
|
Nr
|
Data
|
Zagadnienia
|
Do poczytania
|
Zadania
|
|
1.
|
27.11.2009
|
Logical Framework LF i jego implementacja - Twelf
Reprezentacje pierwszego rzędu w Twelfie na przykładzie liczb naturalnych
|
[3]
Proving metatheorems with Twelf (część 1)
|
lista 1
|
|
2.
|
04.12.2009
|
Reprezentacje wyższego rzędu w Twelfie na przykładzie języka MiniML
|
Proving metatheorems with Twelf (część 2)
[2] (rozdzial 3)
|
lista 2
|
|
3.
|
11.12.2009
|
Sądy hipotetyczne i parametryczne na przykładzie rachunku lambda z typami prostymi
Wnioskowanie w niepustych kontekstach
|
[2] (rozdzial 5)
[4]
|
lista 3
|
|
4.
|
18.12.2009
|
Zawieranie się światów
|
[4]
|
lista 4
|
Termin przesyłania rozwiązań zadań z list 1-4 upływa 24.01.2010.
|
|