Jui-Hsuan Wu (Ray) 吳睿軒

PhD student | Institut Polytechnique de Paris & Inria Saclay



Hi! I am Jui-Hsuan Wu, a third-year PhD student at LIX, Ecole Polytechnique & Inria Saclay advised by Dale Miller and Beniamino Accattoli. I also go by the name Ray.

Before, I studied computer science and mathematics at Ecole Normale Supérieure and got a master degree from Master Parisien de Recherche en Informatique. You can have a look at my CV (Version française).

Research topic

I am working on term representations based on proof theory.

Terms (or expressions) are essential in many different settings: mathematical proofs, programming languages, proof assistants and so on. Proof theory has been widely used to motivate the design of term structures.

The goal of my PhD project is to build a logical framework based on proof theory to describe/unify/justify different term representations, in the hope that proof-theoretic considerations will on one hand provide careful and formal descriptions of term structures and on the other hand give us more insights on terms.

Instead of using proof systems such as Gentzen’s natural deduction and sequent calculus, we use the focused proof system LJF in order to give more structure to proofs. The notion of polarization gives the flexibility to construct differents forms of proofs, which is a desirable feature since we want to describe different term structures in our system.

I am also working on graphical representations for terms related to the term structures obtained as described above.

Some problems I am thinking about:

  • How can terms (proofs) built using different polarization interact with each other?

  • How can terms (proofs) built using different axioms interact with each other?


I am from New Taipei, Taiwan.

Find out how my name is pronouced: Jui, 睿 (sounds like ray in English) and Hsuan, 軒.

Take a look at APLL, an automated prover for linear logic designed and implemented by me.

I am a music enthusiast. I mainly listen to Hip Hop, R&B and Jazz. My favorite artists are Soft Lipa, Loyle Carner, FKJ, Mac Miller, H.E.R., Nick Hakim, …

My brother is a freelance image maker, check out his works here.


Dec 15, 2023 On 18 January 2024, I will give a talk at Syntax Meets Semantics @ IRIF, Paris, France.
Nov 27, 2023 I gave a talk on my recent paper “Proofs as Terms, Terms as Graphs” at APLAS 2023, Taipei, Taiwan. Slides.
Aug 1, 2022 I gave the talk “A positive perspective on term representation: work in progress” at LFMTP 2022, Haifa, Israel. Slides.
Jun 27, 2022 I gave the talk “A positive perspective on term representation” at Proofs and Algorithms seminar, LIX/Inria Saclay (online). Slides.
Oct 1, 2021 I joined the PARTOUT team at Inria Saclay as a PhD student.

Publications & preprints

  1. APLAS 2023
    Proofs as Terms, Terms as Graphs
    Wu, Jui-Hsuan
    In 21st Asian Symposium on Programming Languages and Systems (APLAS). 2023
  2. CSL 2023
    A positive perspective on term representation: Extended paper
    Miller, Dale, and Wu, Jui-Hsuan
    In 31th EACSL Annual Conference on Computer Science Logic (CSL) 2023
  3. LFMTP 2022
    A positive perspective on term representation: work in progress
    Miller, Dale, and Wu, Jui-Hsuan
  4. LICS 2021
    Combinatorial Proofs and Decomposition Theorems for First-order Logic
    Hughes, Dominic, Straßburger, Lutz, and Wu, Jui-Hsuan
    In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021