Inhabitation in System F with simple instantiations

Prelegent(ci)

Aleksy Schubert

Afiliacja

MIMUW

Język referatu

angielski

Termin

11 kwietnia 2025 12:15

Pokój

p. 5450

Tytuł w języku polskim

Inhabitacja w Systemie F z prostym instancjonowaniem

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Rozważany będzie fragment Systemu F, w którym kwantyfikatory ogólne mogą pojawiać sie tylko na negatywnych pozycjach, a zmienne zdaniowe mogą być instancjonowane tylko przez typy proste. Pokazane zostanie, że problem inhabitacji dla tego fragmentu jest rozstrzygalny w Tower.

---

We consider the fragment of System F where universal quantifiers may occur only on negative positions and propositional variables may only be instantiated by simple types. The inhabitation problem for this fragment is proved to be decidable in Tower.

---