Local and asynchronous beta-reduction (an analysis of Girard's execution formula)
Vincent Danos, Laurent Régnier · 2002
The authors build a confluent, local, asynchronous reduction on lambda -terms, using infinite objects (partial injections of Girard's (1988) algebra L*), which is simple (only one move), intelligible (semantic setting of the reduction), and general (based on a large-scale decomposition of beta ), and may be mechanized.>