DocumentCode
1822577
Title
Local and asynchronous beta-reduction (an analysis of Girard´s execution formula)
Author
Danos, Vincent ; Regnier, Laurent
Author_Institution
Paris VII Univ., France
fYear
1993
fDate
19-23 Jun 1993
Firstpage
296
Lastpage
306
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
Keywords
lambda calculus; λ-terms; Girard´s execution formula; L* algebra; confluent local asynchronous beta-reduction; infinite objects; large-scale decomposition; mechanizabilty; partial injections; semantic setting; single move reduction; Algebra; Geometry; Glass; Large-scale systems; Logic; Microscopy;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location
Montreal, Que.
Print_ISBN
0-8186-3140-6
Type
conf
DOI
10.1109/LICS.1993.287578
Filename
287578
Link To Document