Nierozstrzygalność semiunifikacji na chuseczce do nosa

Speaker(s)

Aleksy Schubert

Affiliation

MIMUW

Date

Oct. 8, 2021, 12:15 p.m.

Room

room 5820

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---