Lics

IEEE Symposium on Logic in Computer Science

Paper: Local and asynchronous beta-reduction (an analysis of Girard's execution formula) (at LICS 1993)

Abstract

The authors build a confluent, local, asynchronous reduction on λ-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 β), and may be mechanized

BibTeX

 @InProceedings{DanosRegnier-Localandasynchronou,
 author = 	 {Vincent Danos and Laurent Regnier},
 title = 	 {Local and asynchronous beta-reduction (an analysis of Girard's execution formula) },
 booktitle = {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
 year =	 {1993},
 month =	 {June}, 
 pages = {296--306},
 location = {Montreal, Canada}, 
 publisher =	 {IEEE Computer Society Press}
 }