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

Authors: Vincent Danos Laurent Regnier

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}
  }