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.
2006
International Conference on Foundations of Software Science and Computation Structures -- FOSSACS 2006
Vienna, Austria
March, 25-31
Foundations of Software Science and Computation Structures
Springer Verlag
3921
367
381
http://www.di.unito.it/~paolini/
http://www.di.unito.it/~ronchi/
http://www.springerlink.com/content/jn67771j88n48411/
call by value; strong normalization; parametric lambda calculus
L. PAOLINI; E. PIMENTEL; S. RONCHI DELLA ROCCA
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1701
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact