After introducing the syntax for a version of second order typed lambda calculus (Girard's system F plus product types and a terminal type), we give a categorical presentation of the coherence spaces model of polymorphism as a PLF-category, a generalization of Seely's PL-categories, whose class provides a complete semantics for second order lambda calculus.
Some aspects of the categorical semantics for the polymorphic lambda calculus.
MAIETTI, MARIA EMILIA
1996
Abstract
After introducing the syntax for a version of second order typed lambda calculus (Girard's system F plus product types and a terminal type), we give a categorical presentation of the coherence spaces model of polymorphism as a PLF-category, a generalization of Seely's PL-categories, whose class provides a complete semantics for second order lambda calculus.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
