Inhabitation in System F with simple instantiations

Speaker(s)

Aleksy Schubert

Affiliation

MIMUW

Language of the talk

English

Date

April 11, 2025, 12:15 p.m.

Room

room 5450

Title in Polish

Inhabitacja w Systemie F z prostym instancjonowaniem

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---

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.

---