Jui-Hsuan WU

I am currently a PhD student in Computer Science at LIX, Ecole Polytechnique. My advisor is Dale Miller. I am particularly interested in proof theory, programming language theory, and verification.

• Education

  2021 -
  PhD student in Computer Science, École Polytechnique, Palaiseau, France
  2019 - 2020
  Master 2 (M.Sc.) in Computer Science, École Normale Supérieure and MPRI , Paris, France
  2018 - 2019
  Master 1 in Computer Science, École Normale Supérieure and MPRI , Paris, France
  2017 - 2018
  Licence 3 (B.Sc.) in Computer Science, École Normale Supérieure and Paris Diderot University, Paris, France
  2017 - 2021
  Élève normalien, École Normale Supérieure, Paris, France.
  2015 - 2017
  CPGE, Lycée Janson-de-Sailly, Paris, France

• Research interests

  Proof theory, Lambda calculus, Functional programming, Type theory, Automated theorem proving, Verification.

• Publications

  • Combinatorial Proofs and Decomposition Theorems for First Order Logic, 2021, with Lutz Straßburger and Dominic Hughes. In proceedings of LICS 2021.

• Misc

  • M2 internship report : Internship about first-order combinatorial proofs and deep inference under the supervision of Lutz Straßburger.
  • M1 internship report : Internship about checking subject reduction in lambda-pi-calculus modulo rewriting under the supervision of Frédéric Blanqui and Valentin Blot.
  • APLL : a focusing-based Automated Prover for Linear Logic
    This prover for linear logic gives users the possibility of generating proof certificates that guarantee the validity of proofs by using the proof assistant Coq and the Yalla library.
    Here are the slides from my talk at the workshop on "Machine Proofs of Linear Logic". You can find more details here.

• Curriculum Vitae

  My CV can be downloaded here: English version/ Version française.