JVM w Coqu po mojemu czyli faktoryzacja faktoryzacji

Prelegent(ci)

Patryk Czarnik

Afiliacja

Uniwersytet Warszawski

Termin

9 stycznia 2012 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Chodzi oczywiście o formalizację w Coqu semantyki maszyny wirtualnej Javy.

Ogólnie będzie... jak zwykle, a w szczegółach - jak realizuję operacje na stosie wartości (tzw. stackop) i jakie wnioski z tego wynikają dla całej formalizacji.

---