nLab Nick Benton

• webpage

Selected writings

On categorical semantics for the exponential modality in linear logic:

• Nick Benton, Gavin Bierman, Valeria de Paiva, Term assignment for intuitionistic linear logic, Technical report 262, Computer Laboratory, University of Cambridge (August 1992) [pdf, pdf]

  (published abridged as BBPH92)

• Nick Benton, Gavin Bierman, Valeria de Paiva, Martin Hyland, Linear $\lambda$-Calculus and Categorical Models Revisited, in Computer Science Logic. CSL 1992, Lecture Notes in Computer Science 702, Springer (1993) [doi:10.1007/3-540-56992-8_6]

and specifically as the comonad induced from an adjunction between ordinary types and linear types:

• Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]

On modal operator-like monads in computer science:

• Nick Benton, Gavin Bierman, Valeria de Paiva, Computational Types from a Logical Perspective, Journal of Functional Programming 8 2 (1998) 177-193 [doi:10.1017/S0956796898002998, web]

On monads in computer science:

• Nick Benton, John Hughes, Eugenio Moggi, Monads and Effects, in: Applied Semantics, Lecture Notes in Computer Science 2395, Springer (2002) 42-122 [doi:10.1007/3-540-45699-6_2]

• Nick Benton, Categorical Monads and Computer Programming, in: Impact150: stories of the impact of mathematics. London Mathematical Society (2015) [pdf, pdf, doi:10.1112/i150lms/t.0002]

On dependent linear type theory:

• Neelakantan Krishnaswami, Pierre Pradic, Nick Benton, Integrating Dependent and Linear Types, ACM SIGPLAN Notices 50 1 (2015) 17–30 [pdf, doi:10.1145/2775051.2676969]

Related entries

• linear type theory

• dependent linear type theory

category: people