Proof nets and explicit substitutions Using various translations of the $\l$-calculus into proof nets, new abstract machines have been proposed that exploit the Geometry of Interaction and Dynamic Algebras (Girard 1989; Abramsky and Jagadeesan 1992; Danos 1990), leading to work on optimal reduction (Gonthier et al. 1992; Lamping 1990)

• Autores: DELIA KESNER, ROBERTO DI COSMO, EMMANUEL POLONOVSKI
• Localización: Mathematical structures in computer science, ISSN 0960-1295, Vol. 13, Nº 3, 2003, págs. 409-450
• Idioma: inglés
• DOI: 10.1017/s0960129502003791
• Texto completo no disponible (Saber más ...)