Nie jesteś zalogowany | Zaloguj się

Higher-order matching, transformations T1 and T2 and 4th order matching

Prelegent(ci)
Aleksy Schubert
Afiliacja
MIMUW
Język referatu
angielski
Termin
29 listopada 2024 12:15
Pokój
p. 5450
Tytuł w języku polskim
Dopasowanie wyższego rzędu, transformacje T1 i T2 oraz dopasowanie czwartego rzędu
Seminarium
Seminarium „Logika i teoria typów”


Stirling's proof of the higher-order matching decidability
uses two basic solution transformations called T1 and T2
and then the third transformation called unfolding. The vocabulary
introduced on the previous talk will make it easy to formulate
the first two of them. After that I will present how to use these
to prove that the fourth-order matching is decidable.