Scott’s information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a “set-theoretic” interpretation of exponentials that recovers Scott continuous functions via the co-Kleisli construction. From a domain theoretic point of view, linear information systems are equivalent to prime algebraic Scott domains, which in turn generalize prime algebraic lattices, already known to provide a model of classical linear logic.
On linear information systems
CARRARO, ALBERTO;SALIBRA, Antonino
2010-01-01
Abstract
Scott’s information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a “set-theoretic” interpretation of exponentials that recovers Scott continuous functions via the co-Kleisli construction. From a domain theoretic point of view, linear information systems are equivalent to prime algebraic Scott domains, which in turn generalize prime algebraic lattices, already known to provide a model of classical linear logic.File | Dimensione | Formato | |
---|---|---|---|
Linearity09-EPTCS.pdf
accesso aperto
Tipologia:
Abstract
Licenza:
Licenza non definita
Dimensione
192.46 kB
Formato
Adobe PDF
|
192.46 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.