Higher-order matching, unfolding and recapitulation
- Prelegent(ci)
- Aleksy Schubert
- Afiliacja
- MIMUW
- Język referatu
- angielski
- Termin
- 6 grudnia 2024 12:15
- Pokój
- p. 5450
- Tytuł w języku polskim
- Dopasowanie wyższego rzędu, rozwijanie i podsumowanie
- Seminarium
- Seminarium „Logika i teoria typów”
The third transformation in Stirling's proof of the higher-order
matching decidability is called unfolding. I will present its
definition and I will sketch the final recapitulation of the
Stirling's proof. Notably, the transformation is defined in
terms of computation history (aka play). In this way we obtain
the guarantee that the transformation leads to a solution.