Jyun-Ao Lin's Homepage
This site is always under construction….
Personal info
I'm currently an assistant professor in the CSIE and iFIRST of NTUT. Prior joining NTUT, I was a post-doc researcher in K.-M. Chung's Lab at IIS, Academia Sinica. Before switching my interests to computer science, I was a post-doc researcher at IoM, Academia Sinica. I defended my Ph.D. thesis in IMJ-PRG and Universite de Paris-Diderot Paris VII, under the supervission of Prof. Marc Rosso and Prof. Olivier Schiffmann.
- Email: jalin[at]ntut.edu.tw
- Phone: +886-2-2771-2171 #5715
- Address: 13F, Pioneer International R&D Building, 46, Sec. 3, Zhongxiao E. Rd., Taipei 10608 Taiwan
Research Interests
quantum program verification, automated reasoning, decision procedure of SMT, cryptography, quantum computing and representation theory.
News
I am currently looking for talented and self-motivated students in formal verification, (privacy-preserving) decision procedure and/or quantum program. If you are interested in working with me, please do not hesitate to contact me via email.
Publications
see DBLP for more details
Recent Journal and Conferences
- Y. F. Chen, K.-M. Chung, M.-H. Hsieh, W.-J. Huang, O. Lengal, J.-A. Lin, W.-L. Tsai, AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs, submitted, 2024, arxiv
- P. A. Abdulla, Y.-C. Chen, Y.-F. Cheng, L. Holik, O. Lengal, J.-A. Lin, F.-Y. Lo, W.-L. Tsai, Verifying Quantum Circuits with Level-Synchronized Tree Automata, POPL 2025, Technical Report,
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, AutoQ: An Automata-based Quantum Circuit Verifier, CAV 2023 link
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, D.-D. Yen, An Autamata-based Framework for Verification and Bug Hunting in Quantum Circuits, Distinguished Paper Award, PLDI 2023. link, Technical Report
Extended Abstracts
- Y.-F. Chen, K.-M. Chung, O. Lengal, J.-A. Lin, W.-L. Tsai, D.-D. Yen, An Autamata-based Framework for Verification and Bug Hunting in Quantum Circuits, QPL 2023.
Old math publications
- J.-A. Lin, Spherical Hall algebra of a weighted projective curve, International Mathematics Research Notices, (SCI) https://doi.org/10.1093/imrn/rny158, Vol. 2020, Issue 15, Aug. 2020, 4721–4775.
- J.-A. Lin, A new involution for quantum loop algebras, Journal of Algebra, (SCI) vol. 480, (2017), 368–384.
Awards
- Distinguished paper award PLDI 2023
- Post-doc Outstanding Research Award MOST 2018
Services
PC Duties
- 2025: TASE
Teaching
at NTUT
- Compilers (2024 Fall, NTUT)
- Computational Logic and Software Verification (2024 Spring, NTUT)
- Formal Language (2024 Fall, 2024 Spring, NTUT)
Past
- Theorical Aspects of Modern Cryptograpgy (2021 Spring, 2022 Spring, 2023 Spring NTU CSIE)
- Calculus A (2017-2018 MATH NTU, 2020 Spring XMU Malaysia)
- Advanced Mathematics (2020 Spring, XMU Malaysia)
- Algebra and Analytic Geometry (2019 Fall, XMU Malaysia)
- Engineering Mathematics III (2019 Fall, XMU Malaysia)
- Multi Variables Calculus (2020 Spring, XMU Malaysia)
- Fourier Analysis for physics (2014 Spring, TA Universite de Paris-Sud Orsay)
- WIMS session for Linear Algebras (2014 Spring, TA Universite de Paris-Sud Orsay)
- S1 Mathematics (2013 Fall, TA, Universite de Paris-Sud Orsay)
Tools
- AutoQ: An automata-based C++ tool for quantum program verification.