Seminarium Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji (SLIWOWICA)

Prelegent: Patryk Czarnik

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.