| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Sat, 18 Oct 2025 15:52:51 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"68f3b7d3-2595"
expires: Mon, 29 Dec 2025 16:47:44 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: C48D:3946E9:9079C2:A22A75:6952AE58
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 16:37:44 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210020-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767026265.737186,VS0,VE222
vary: Accept-Encoding
x-fastly-request-id: a7c26c752a9d322e7f44ba311d1fd59f451c5f35
content-length: 3015
Cheng-Syuan Wan
Last update 18.10.2025
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.
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
- C.-S. Wan. Semi-substructural logics à la Lambek with symmetry.
Bulletin of the Section of Logic, to appear, 2025. - 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 pdf - N. Veltri, C.-S. Wan. Craig Interpolation for a semi-substructural logic.
Studia Logica, to appear, 2025.
Agda code pdf - 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 - 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 - 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
PhD Thesis
-
C.-S. Wan. Proof Theory of Semi-Substructural Logics.
Doctoral Thesis, Tallinn University of Technology, 2025.
Agda code Taltech Digital Library
Presentations
- 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
- PACM∧N'25, Rome.
- Semi-Substructural Logics à la Lambek at
- NCL'24, Łódź.
- Craig Interpolation for Semi-Substructural Logics at
- 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.