@inproceedings(AS:norecp,
 author       = {Andreas Abel and Christian Sattler},
 year         = {2019},
 title        = {Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda Calculus},
 editor       = {Ekaterina Komendantskaya},
 booktitle    = {Proceedings of the 21st International Symp. on Principles and Practice of Programming Languages, PPDP 2019},
 publisher    = {{ACM}},
 pages        = {3:1--3:12},
 doi          = {10.1145/3354166.3354168},
)
@article(Abr:noncil,
 author       = {Vito M. Abrusci},
 year         = {1990},
 title        = {Non\IeC{-}Commutative Intuitionistic Linear Logic},
 journal      = {Mathematical Logic Quarterly},
 volume       = {36},
 number       = {4},
 pages        = {297--318},
 doi          = {10.1002/malq.19900360405},
)
@inproceedings(ADHS:noretl,
 author       = {Thorsten Altenkirch and Peter Dybjer and Martin Hofmann and Philip J. Scott},
 year         = {2001},
 title        = {Normalization by Evaluation for Typed Lambda Calculus with Coproducts},
 booktitle    = {Proceedings of the 16th Annual {IEEE} Symp. on Logic in Computer Science, LICS 2001},
 publisher    = {{IEEE} Computer Society},
 pages        = {303--310},
 doi          = {10.1109/LICS.2001.932506},
)
@inproceedings(AHS:catrrf,
 author       = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
 year         = {1995},
 title        = {Categorical Reconstruction of a Reduction Free Normalization Proof},
 editor       = {David H. Pitt and David E. Rydeheard and Peter T. Johnstone},
 booktitle    = {Proceedings of the 6th International Conference on Category Theory and Computer Science, {CTCS} 1995},
 series       = {Lecture Notes in Computer Science},
 volume       = {953},
 publisher    = {Springer},
 pages        = {182--199},
 doi          = {10.1007/3-540-60164-3\_27},
)
@inproceedings(AU:nore,
 author       = {Thorsten Altenkirch and Tarmo Uustalu},
 year         = {2004},
 title        = {Normalization by Evaluation for $\lambda$$^{\unhbox\voidb@x \hbox{${\to}2$}}$},
 editor       = {Yukiyoshi Kameyama and Peter J. Stuckey},
 booktitle    = {Proceedings of the 7th International Symp. on Functional and Logic Programming, {FLOPS} 2004},
 series       = {Lecture Notes in Computer Science},
 volume       = {2998},
 publisher    = {Springer},
 pages        = {260--275},
 doi          = {10.1007/978-3-540-24754-8\_19},
)
@article(AR:norspl,
 author       = {Maxime Amblard and Christian Retor{\'{e}}},
 year         = {2014},
 title        = {Partially Commutative Linear Logic and Lambek Caculus with Product: Natural Deduction, Normalisation, Subformula Property},
 journal      = {{FLAP}},
 volume       = {1},
 number       = {1},
 pages        = {53--94},
 url          = {http://www.collegepublications.co.uk/downloads/ifcolog00001.pdf},
)
@inproceedings(BCF:extntd,
 author       = {Vincent Balat and Roberto Di Cosmo and Marcelo P. Fiore},
 year         = {2004},
 title        = {Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums},
 editor       = {Neil D. Jones and Xavier Leroy},
 booktitle    = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2004},
 publisher    = {{ACM}},
 pages        = {64--76},
 doi          = {10.1145/964001.964007},
)
@phdthesis(BP:duaill,
 author       = {Andrew G. Barber},
 year         = {1997},
 title        = {Linear Type Theories, Semantics and Action Calculi},
 school       = {University of Edinburgh, {UK}},
 url          = {http://hdl.handle.net/1842/392},
)
@inproceedings(BBdePH:tercil,
 author       = {Nick Benton and Gavin M. Bierman and Valeria de Paiva and Martin Hyland},
 year         = {1993},
 title        = {A Term Calculus for Intuitionistic Linear Logic},
 editor       = {Marc Bezem and Jan Friso Groote},
 booktitle    = {Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, {TLCA} '93},
 series       = {Lecture Notes in Computer Science},
 volume       = {664},
 publisher    = {Springer},
 pages        = {75--90},
 doi          = {10.1007/BFb0037099},
)
@inproceedings(BS:inveft,
 author       = {Ulrich Berger and Helmut Schwichtenberg},
 year         = {1991},
 title        = {An Inverse of the Evaluation Functional for Typed lambda-calculus},
 booktitle    = {Proceedings of the 6th Annual Symposium on Logic in Computer Science, {LICS} 1991},
 publisher    = {{IEEE} Computer Society},
 pages        = {203--211},
 doi          = {10.1109/LICS.1991.151645},
)
@inproceedings(BNS:focnd,
 author       = {Brock{-}Nannestad, Taus and Carsten Sch{\"{u}}rmann},
 year         = {2010},
 title        = {Focused Natural Deduction},
 editor       = {Christian G. Ferm{\"{u}}ller and Andrei Voronkov},
 booktitle    = {Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, {LPAR} 2010},
 series       = {Lecture Notes in Computer Science},
 volume       = {6397},
 publisher    = {Springer},
 pages        = {157--171},
 doi          = {10.1007/978-3-642-16242-8\_12},
)
@inproceedings(Fio:semane,
 author       = {Marcelo P. Fiore},
 year         = {2002},
 title        = {Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus},
 booktitle    = {Proceedings of the 4th International {ACM} {SIGPLAN} Conference on Principles and Practice of Declarative Programming, {PPDP} 2002},
 publisher    = {{ACM}},
 pages        = {26--37},
 doi          = {10.1145/571157.571161},
)
@inproceedings(Has:logpil,
 author       = {Masahito Hasegawa},
 year         = {1999},
 title        = {Logical Predicates for Intuitionistic Linear Type Theories},
 editor       = {Jean{-}Yves Girard},
 booktitle    = {Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, {TLCA} 1999},
 series       = {Lecture Notes in Computer Science},
 volume       = {1581},
 publisher    = {Springer},
 pages        = {198--212},
 doi          = {10.1007/3-540-48959-2\_15},
)
@inproceedings(Hep:norftp,
 author       = {Mark Hepple},
 year         = {1990},
 title        = {Normal Form Theorem Proving for the Lambek Calculus},
 booktitle    = {Proceedings of the 13th International Conference on Computational Linguistics, {COLING} 1990},
 pages        = {173--178},
 url          = {https://aclanthology.org/C90-2030/},
)
@article(HS:gluoml,
 author       = {Martin Hyland and Andrea Schalk},
 year         = {2003},
 title        = {Glueing and Orthogonality for Models of Linear Logic},
 journal      = {Theorerical Computer Science},
 volume       = {294},
 number       = {1/2},
 pages        = {183--231},
 doi          = {10.1016/S0304-3975(01)00241-9},
)
@inproceedings(LR:pronlc,
 author       = {Francois Lamarche and Christian Retor{\'e}},
 year         = {1996},
 title        = {Proof Nets for the Lambek Calculus -- an Overview},
 booktitle    = {Proceedings of the 3rd Roma Workshop on Proofs and Linguistic Categories 1998},
 pages        = {241--262},
 url          = {https://hal.archives-ouvertes.fr/inria-00098442},
)
@article(Lam:matss,
 author       = {Joachim Lambek},
 year         = {1958},
 title        = {The Mathematics of Sentence Structure},
 journal      = {The American Mathematical Monthly},
 volume       = {65},
 number       = {3},
 pages        = {154--170},
 doi          = {10.2307/2310058},
)
@article(Lam:ded1,
 author       = {Joachim Lambek},
 year         = {1968},
 title        = {Deductive Systems and Categories {I}: Syntactic Calculus and Residuated Categories},
 journal      = {Mathematical Systems Theory},
 volume       = {2},
 number       = {4},
 pages        = {287--318},
 doi          = {10.1007/bf01703261},
)
@incollection(Lam:ded2,
 author       = {Joachim Lambek},
 year         = {1969},
 title        = {Deductive Systems and Categories {II}: Standard Constructions and Closed Categories},
 booktitle    = {Category theory, Homology Theory and Their Applications {I}},
 publisher    = {Springer},
 pages        = {76--122},
 doi          = {10.1007/bfb0079385},
)
@phdthesis(Pol:ordlla,
 author       = {Jeff Polakov},
 year         = {2001},
 title        = {Ordered Linear Logic and Applications},
 school       = {Carnegie Mellon University, {USA}},
 url          = {https://www.cs.cmu.edu/~jpolakow/diss.ps},
)
@inproceedings(PP:natdin,
 author       = {Jeff Polakow and Frank Pfenning},
 year         = {1999},
 title        = {Natural Deduction for Intuitionistic Non-communicative Linear Logic},
 editor       = {Jean{-}Yves Girard},
 booktitle    = {Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, {TLCA} 1999},
 series       = {Lecture Notes in Computer Science},
 volume       = {1581},
 publisher    = {Springer},
 pages        = {295--309},
 doi          = {10.1007/3-540-48959-2\_21},
)
@article(Roo:pronlc,
 author       = {Dirk Roorda},
 year         = {1992},
 title        = {Proof Nets for Lambek Calculus},
 journal      = {Journal of Logic and Computation},
 volume       = {2},
 number       = {2},
 pages        = {211--231},
 doi          = {10.1093/logcom/2.2.211},
)
@inproceedings(UVZ:dedscs,
 author       = {Tarmo Uustalu and Niccol{\'o} Veltri and Noam Zeilberger},
 year         = {2021},
 title        = {Deductive Systems and Coherence for Skew Prounital Closed Categories},
 editor       = {{Sacerdoti Coen}, Claudio and Alwen Tiu},
 booktitle    = {Proceedings of the 15th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {332},
 publisher    = {Open Publishing Assoc.},
 pages        = {35--53},
 doi          = {10.4204/eptcs.332.3},
)
@inproceedings(VR:expebc,
 author       = {Nachiappan Valliappan and Alejandro Russo},
 year         = {2019},
 title        = {Exponential Elimination for Bicartesian Closed Categorical Combinators},
 editor       = {Ekaterina Komendantskaya},
 booktitle    = {Proceedings of the 21st International Symp. on Principles and Practice of Programming Languages, {PPDP} 2019},
 publisher    = {{ACM}},
 pages        = {20:1--20:13},
 doi          = {10.1145/3354166.3354185},
)