Title :
Local and asynchronous beta-reduction (an analysis of Girard´s execution formula)
Author :
Danos, Vincent ; Regnier, Laurent
Author_Institution :
Paris VII Univ., France
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;
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
DOI :
10.1109/LICS.1993.287578
