Mały bajtkod

Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje są sparametryzowane, aby móc reprezentować wszystkie instrukcje oryginalnego języka, a wybór 12 instrukcji jest oparty o sposób korzystania ze struktur danych JVM.

Staraliśmy się pokryć cały język JVML i co najmniej umożliwić uwzględnienie wszystkich aspektów, takich jak współbieżność czy Java Memory Model. Na seminarium przedstawione zostaną też pomysły na dalsze rozwinięcie tego tematu w kierunku formalizcji tej pracy w Coqu, wykorzystania do analiz statycznych/abstrakcyjnych interpretacji, czy opracowania analogicznie "skompresowanego" języka specyfikacji dla JVM.