The paper introduces the Φ-calculus, a new call-by-value version of λ-calculus, following the spirit of Plotkin's λβv-calculus. Such a language satisfies some properties, in particular the set of solvable terms in it coincides with the set of β-strongly normalizing terms in the classical λ-calculus.
An Operational Characterization of Strong Normalization
PAOLINI, LUCA LUIGI;RONCHI DELLA ROCCA, Simonetta
2006-01-01
Abstract
The paper introduces the Φ-calculus, a new call-by-value version of λ-calculus, following the spirit of Plotkin's λβv-calculus. Such a language satisfies some properties, in particular the set of solvable terms in it coincides with the set of β-strongly normalizing terms in the classical λ-calculus.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
Operational Characterization of Strong Normalization - LNCS 2006 ori.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
471.18 kB
Formato
Adobe PDF
|
471.18 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.