You are not logged in |
Higher-order matching, unfolding and recapitulation
- Speaker(s)
- Aleksy Schubert
- Affiliation
- MIMUW
- Language of the talk
- English
- Date
- Dec. 6, 2024, 12:15 p.m.
- Room
- room 5450
- Title in Polish
- Dopasowanie wyższego rzędu, rozwijanie i podsumowanie
- Seminar
- Seminar Semantics, Logic, Verification and its Applications
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.
