Nierozstrzygalność semiunifikacji na chuseczce do nosa

Prelegent(ci)

Aleksy Schubert

Afiliacja

MIMUW

Termin

8 października 2021 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Problem semiunifikacji pojawia się naturalnie w zagadnieniach związanych z typowalnością programów funkcyjnych, w których systemy typów opartych na systemie F. Intuicyjnie chodzi tutaj o typowanie, w którym funkcji w programie staramy się przypisać jak najbardziej ogólny typ, a potem w miejscu użycia pozwalamy, aby ten typ został uszczegółowiony zgodnie z konkretnymi potrzebami. Niedawno Andrej Dudenhefner opublikował bardzo zgrabny i krótki dowód nierozstrzygalności problemu seminunifikacji. Zostanie przedstawiony właśnie ten dowód.

---