Linear dependent types were introduced recently as a formal system that allows to precisely capture both the extensional behavior and the time complexity of λ-terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value computation. A system of linear dependent types for Plotkin's PCF is introduced, called dℓPCFV, whose types reflect the complexity of evaluating terms in the CEK machine. dℓPCFV is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.

Linear dependent types in a call-by-value scenario

DAL LAGO, UGO;
2014

Abstract

Linear dependent types were introduced recently as a formal system that allows to precisely capture both the extensional behavior and the time complexity of λ-terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value computation. A system of linear dependent types for Plotkin's PCF is introduced, called dℓPCFV, whose types reflect the complexity of evaluating terms in the CEK machine. dℓPCFV is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.
2014
Dal Lago, Ugo; Petit, Barbara
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/338521
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 5
social impact