Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
Balat, Vincent ; Di Cosmo, Roberto ; Fiore, Marcelo
HAL, hal-00149561 / Harvested from HAL
Text on HAL
We present a notion of η-long β-normal term for the typed lambda calculus with sums and prove, using Grothendieck logical relations, that every term is equivalent to one in normal form. Based on this development we give the first type-directed partial evaluator that constructs %able to construct normal forms of terms in this calculus.
Publié le : 2004-01-01
Classification:  [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL],  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] 
@article{hal-00149561,
     author = {Balat, Vincent and Di Cosmo, Roberto and Fiore, Marcelo},
     title = {Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums},
     journal = {HAL},
     volume = {2004},
     number = {0},
     year = {2004},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00149561}
}

Balat, Vincent; Di Cosmo, Roberto; Fiore, Marcelo. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00149561/