Cheng-Syuan Wan

I am a researcher in the Logic and Semantics Group at Tallinn University of Technology.
I was a PhD student in the same group during January 2021 to June 2025. My supervisors were Tarmo Uustalu and Niccolò Veltri.

Contact

Email:	cswan at cs ioc ee
Address:	B424, Akadeemia tee 21b, 12618 Tallinn, Estonia

Research Interests

Structural proof theory, substructural logic, categorical and algebraic semantics, formalization of mathematics.

Publications

1. 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), Lect. Notes in Comput. Sci., Springer, to appear.
   Agda code
2. N. Veltri, C.-S. Wan. Craig Interpolation for a semi-substructural logic.
   Studia Logica, to appear, 2025.
   Agda code pdf
3. 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.
   pdf
4. 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 pdf
5. 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 pdf

Manuscripts

1. C.-S Wan. Semi-Substructural Logics à la Lambek with Symmetry
   pdf

Presentations

• An Agda formalization of nonassociative Lambek calculus and its metatheory at
  • CLoCk'25, Kraków.
• Proof Theory of Semi-Substructural Logics at
  • 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.