Positive Focusing is Directly Useful - Institut Polytechnique de Paris
Pré-Publication, Document De Travail Année : 2024

Positive Focusing is Directly Useful

Résumé

Recently, Miller and Wu introduced the positive λ-calculus, a call-by-value λ-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive λ-calculus stands out among λ- calculi with sharing for a compactness property related to the sharing of variables. We show that—thanks to compactness—the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.
Fichier principal
Vignette du fichier
main.pdf (762.4 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04606194 , version 1 (10-06-2024)

Identifiants

  • HAL Id : hal-04606194 , version 1

Citer

Beniamino Accattoli, Jui-Hsuan Wu. Positive Focusing is Directly Useful. 2024. ⟨hal-04606194⟩
116 Consultations
60 Téléchargements

Partager

More