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