[Prev][Next][Index][Thread]
local and asynchronous beta-reduction
We build a confluent, local, asynchronous reduction on lambda-terms, using
infinite objects (partial one-to-one transformations in Girard's algebra
Lambda*), which is simple (only one move), intelligible (semantic setting of
the reduction), general (based on a large-scale decomposition of beta
reduction), and may be mechanized.
A paper virtred.dvi.Z describing this construction is
ftp-able at frege.logique.jussieu.fr in /pub/scratch/
Vincent Danos & Laurent Regnier.