Head linear reduction is one of the approaches to normalization of lambda-terms, which does not require neither to perform beta-reductions in their classic sense, nor to implement closures or environments. In the talk a HLR-based normalizer for STLC and its generalization for untyped case will be presented.
1. Vincent Danos, Laurent Regnier. Head Linear Reduction, 2004.
2. C.-H. Luke Ong. Normalisation by traversals. CoRR, abs/1511.02629, 2015.
Presenter: Daniil Berezun.
Date: March 28, 2016
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr-t, 28