Nie jesteś zalogowany | Zaloguj się

JVM w Coqu - struktury czasu wykonania

Prelegent(ci)
Patryk Czarnik
Afiliacja
Uniwersytet Warszawski
Termin
28 marca 2011 10:15
Pokój
p. 4790
Seminarium
Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Staram się zaimplementować w Coqu semantykę bajtkodu Javy w wersji wykorzystującej "faktoryzację" i "parametryzację" (bajtkod w 12 instrukcji).

Na seminarium przedstawię definicje typów dla struktur czasu wykonania. Mam nadzieję na dyskusję i rady co do sensowności owijania wszystkiego we własne definicje, ukrywania za sygnaturą itp.