Jui-Hsuan Wu (Ray) 吳睿軒
PhD student | LIX, Ecole Polytechnique & Inria Saclay
About
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 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 well-chosen proof system, 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 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 tree-like 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 let-expressions). 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 cut-free proofs. This means that the usual computation-as-proof-normalization approach would not work in our setting. For this, I proposed another approach which involves some proof transformation (that transforms a cut-free proof into a proof with cuts) and cut-elimination. 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 beta-reduction of the \(\lambda\)-calculus in a meaningful way. Since positive \(\lambda\)-terms involve a number of let-expressions, 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 6-dan 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, …
My brother is a freelance image maker, check out his works here.
News
| 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. |
| Nov 27, 2023 | I gave a talk on my recent paper “Proofs as Terms, Terms as Graphs” at APLAS 2023 @ Academia Sinica, Taipei, Taiwan. 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 First-order LogicIn 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021