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.