Local and asynchronous beta-reduction (an analysis of Girard's execution formula)
- 31 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 296-306
- https://doi.org/10.1109/lics.1993.287578
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: