JuiHsuan Wu (Ray) 吳睿軒
PhD student  LIX, Ecole Polytechnique & Inria Saclay
About
Hi! I am JuiHsuan Wu, a thirdyear 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 interests
 Proof theory
 Logic
 \(\lambda\)calculus
 Functional programming
Current research
I am current working on term representation based on proof theory.
Terms (or expressions) are essential in many different settings: mathematical proofs, programming languages, proof assistants, etc. Proof theory has been widely used to motivate the design of term structures.
The goal of my PhD project is to design/study term structures based on some wellchosen proof system, in the hope that prooftheoretic 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 be able to describe different term structures in our system. In particular, we consider the negative (resp. positive) polarization, that is, the one that assigns the negative (resp. positive) polarity to each atom. This two polarizations induce two very different styles of term structures. Intuitively, the negative polarization yields the usual treelike syntax, without any possible sharing within a term, while the positive polarization yields a syntax where sharing is possible within a term via some specific form of explicit substitutions (or letexpressions). Based on this approach, we also propose a positive presentation of \(\lambda\)terms, called positive \(\lambda\)terms (negative \(\lambda\)terms coincide with usual \(\lambda\)terms). See our CSL2023 paper for more details.
A key point in our CSL paper is that (\(\lambda\))terms correspond to cutfree proofs. This means that the usual computationasproofnormalization approach would not work in our setting. For this, I proposed another approach which involves some proof transformation (that transforms a cutfree proof into a proof with cuts) and cutelimination. Such an approach is however not universal, it is should be seen as a recipe that one could follow and adapt based on his/her purposes. The untyped \(\lambda\)calculus can be defined from negative/usual \(\lambda\)terms in this way. What about positive \(\lambda\)terms? Following a similar idea, I defined the positive \(\lambda\)calculus and show its reduction is compatible with the betareduction of the \(\lambda\)calculus in a meaningful way. Since positive \(\lambda\)terms involve a number of letexpressions, it is natural to consider the equivalence based on permutable or parallel let’s, namely the structural equivalence. For this, I defined \(\lambda\)graphs with bodies, essentially DAGs with some additional structure to deal with bindings, that capture the structural equivalence on positive \(\lambda\)terms. See my APLAS2023 paper for more details.
Recently, I worked with Beniamino Accattoli on a connection between the positive \(\lambda\)calculus and usefulness, a notion of reduction with sharing first introduced to study reasonable cost models. You can find more details in our MFPS2024 paper.
Misc
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 propositional linear logic designed and implemented by me.
I am an amateur go player. I used to be a 6dan player (a long time ago) back in Taiwan.
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, Sunset Rollercoaster, …
I recently got into French touch music: Modjo, Étienne de Crécy, Cassius, Breakbot, and of course the one and only Daft Punk.
My brother is a freelance image maker, check out his works here.
News
Oct 25, 2024  I will be visiting the Institute of Information Science, Academia Sinica and will give a talk on focusing and polarization. 

Jun 21, 2024  I gave a talk at MFPS 2024 @ University of Oxford, UK. Slides and Video. 
Jun 13, 2024  I gave a talk at Proofs and Algorithms Seminar @ LIX, Ecole Polytechnique & Inria Saclay. Slides. 
May 4, 2024  Our paper “Positive Focusing is Directly Useful” (with Beniamino Accattoli) has been accepted at MFPS 2024. 
Jan 18, 2024  I gave a talk at Syntax Meets Semantics @ IRIF, Paris, France. Slides. 
Publications & preprints

MFPS 2024Positive Focusing is Directly UsefulIn 40th International Conference on Mathematical Foundations of Programming Semantics (MFPS). 2024

APLAS 2023Proofs as Terms, Terms as GraphsIn 21st Asian Symposium on Programming Languages and Systems (APLAS). 2023

CSL 2023A positive perspective on term representation: Extended paperIn 31th EACSL Annual Conference on Computer Science Logic (CSL) 2023

LFMTP 2022

LICS 2021Combinatorial Proofs and Decomposition Theorems for Firstorder LogicIn 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021