Simplifying normal functors: an old and a new model of λ-calculus
Résumé
The introduction of Linear Logic by Jean-Yves Girard takes its origins in the so-called normal functors model of lambda-calculus in which untyped λ-terms are interpreted as ‘normal functors’ between presheaf categories. As a result, we produce a new model in ‘normal functions’ between sets of (possibly infinite) multisets, gaining new insights on Girard’s original construction. We then extend this to an explicit model of intuitionistic Linear Logic, contrasting the result with the weighted relational model.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)