Skip to Main content Skip to Navigation
Reports

The Calculus of explicit substitutions lambda-upsilon

Abstract : lambda-upsilon-calculus is a new simple calculus of explicit substitutions. In the paper we explore its properties, namely we prove that it correctly implements B reduction, it is confluent, its simply typed version is strongly normalizing. We associate with it an abstract machine called the U-machine. We prove that it is a correct implementation of the calculus.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074448
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 3:19:14 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 5:00:33 PM

Identifiers

  • HAL Id : inria-00074448, version 1

Collections

Citation

Pierre Lescanne, Jocelyne Rouyer-Degli. The Calculus of explicit substitutions lambda-upsilon. [Research Report] RR-2222, INRIA. 1994. ⟨inria-00074448⟩

Share

Metrics

Record views

144

Files downloads

119