Cheng-Syuan Wan

Publications

1. R. Borsetto, G. Fellin, T. Uustalu, C.-S. Wan. Glivenko's theorem underneath structure.
   In V. Brattka, H. Fernau, L. Galeotti, eds., Proc. of 21st Int. Conf. on Computability in Europe, CiE 2026 (Trier, July 2026), Lect. Notes in Comput. Sci., Springer, to appear.
2. C.-S. Wan. Semi-substructural logics à la Lambek with symmetry.
   Bulletin of the Section of Logic, 2025.
   paper
3. N. Veltri, C.-S. Wan. An Agda formalization of nonassociative Lambek calculus and its metatheory.
   In G. L. Pozzato, T. Uustalu, eds., Proc. of 34th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'25 (Reykjavik, Sept.-Oct. 2025), v. 15980 of Lect. Notes in Comput. Sci., pp. 433-452, Springer, 2025.
   Agda code paper
4. N. Veltri, C.-S. Wan. Craig Interpolation for a semi-substructural logic.
   Studia Logica, to appear, 2025.
   Agda code paper
5. C.-S. Wan. Semi-substructural logics à la Lambek.
   In A. Indrzejczak, M. Zawidzki, eds., Proc. of 11th Int. Conf. on Non-classical Logics: Theory and Applications, NCL 2024 (Lódź, September 2024), v. 415 of Electron. Proc. in Theor. Comput. Sci., pp. 195-213. Open Publishing Assoc., 2024.
   paper
6. N. Veltri, C.-S. Wan. Semi-substructural logics with additives.
   In T. Kutsia, D. Ventura, D. Monniaux, J. F. Morales, eds., Proc. of 18th Int. Wksh. on Logical and Semantic Frameworks with Applications, LSFA 2023 (Rome, July 2023) and 10th Wksh. of Horn Clauses for Verification and Synthesis, HCVS 2023 (Paris, Apr. 2023), v. 402 of Electron. Proc. in Theor. Comput. Sci., pp. 63-80. Open Publishing Assoc., 2024
   Agda code paper
7. T. Uustalu, N. Veltri, C.-S. Wan. Proof theory of skew non-commutative MILL.
   In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL 2022 (Lódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 118-135. Open Publishing Assoc., 2022.
   Agda code paper

PhD Thesis

• C.-S. Wan. Proof Theory of Semi-Substructural Logics.
  Doctoral Thesis, Tallinn University of Technology, 2025.
  Agda code TalTech Digital Library

Presentations

• Proof relevance and well-definedness of Maehara interpolation for Lambek calculi at
  • Logic, models and formal methods Seminar, Palaiseau.
• An Agda formalization of nonassociative Lambek calculus at
  • Theory Days'25, Sigulda.
  • TABLEAUX'25, Reykjavík.
  • CLoCk'25, Kraków.
• Proof Theory of Semi-Substructural Logics at
  • ALC Seminar, Braga.
  • IIS Seminar, Academia Sinica, Taipei.
  • PACM∧N'25, Rome.
• Semi-Substructural Logics à la Lambek at
  • NCL'24, Łódź.
• Craig Interpolation for Semi-Substructural Logics at
  • PS'24, Birmingham.
  • TLLA'24, Tallinn.
• Semi-Substructural Logics with Additives at
  • LSFA'23, Rome.
• Towards Skew Non-Commutative MILL with Additives at
  • LC'23, Milan.
• Skew multiplicative intuitionistic linear logic at
  • PLEXUS Inaugural Conference, Lisbon.
  • WLD'23, Tallinn.
• Proof theory of skew non-commutative MILL at
  • LC'22, Reykjavík.
  • Theory Days'22, Riga.
  • NCL'22, Łódź.
  • WLD'22, Tallinn.