I am a Ph.D. course student in Computer Software Group (Igarashi/Suenaga Laboratory), Department of Communications and Computer Engineering, Graduate School of Informatics, Kyoto University. My current supervisor is Prof. Atsushi Igarashi.

My general research interest is to investigate the Curry–Howard correspondence, focusing on: (1) foundation of programming languages; (2) constructive type theory and constructive proof theory; (3) type-theoretic applications of proof-theoretic semantics. Currently, I've been working on the following topics:

- A geometry of interaction machine for (multi-)staged computation.
- A virtual machine for meta-programming with a first-class macro mechanism.

I have thought that I am a theoretical computer scientist and I **may** **not** be a **non**-logician. (But this can't be "I am a logician." :p)

- Yosuke Fukuda and Akira Yoshimizu. A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4.
In
*Proceedings of Formal Structures for Computation and Deduction (FSCD 2019)*, Dortmund, Germany, June, 2019. [ doi | arXiv | slide ] - Yosuke Fukuda and Ryosuke Igarashi.
A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction.
In
*Proceedings of Logic, Rationality, and Interaction (LORI VI)*, Sapporo, Japan, September, 2017. [ doi | slide ]

- Yosuke Fukuda and Akira Yoshimizu.
A Higher-arity Sequent Calculus for Modal Linear Logic.
In
*RIMS Kôkyûroku No.2083: Symposium on Proof Theory and Proving*, Kyoto, Japan, August, 2018. [ pdf ]

- Yosuke Fukuda. Toward a modalized linear-non-linear model. PPL 2020, Ureshino, Japan, March 3rd, 2020.
- Yosuke Fukuda. Homoiconic Lisp. PPL 2020, Ureshino, Japan, March 2nd, 2020.
- Yosuke Fukuda and Akira Yoshimizu. A Linear-logical Reconstruction of Intuitionistic Modal Logic S4. PPL 2019, Hanamaki, Japan, March 6th, 2019.
- Yosuke Fukuda and Ryosuke Igarashi. A Reconstruction of The Principle of Explosion and Its Computational Structure. PPL 2017, Fuefuki, Japan, March 9th, 2017.
- Yosuke Fukuda and Atsushi Igarashi. Types as Syntactic Specifiactions. APLAS 2015, Pohang, Korea, November 30th, 2015.

- On a computational interpretation of sequent calculus for modal logic S4. Second Workshop on Mathematical Logic and Its Applications, Kanazawa, Japan, March 8th, 2018. [ slide ]

- A geometry of intraction semantics for a modal $\lambda$-calculus. 論理と計算に関する研究集会. Tokyo Metropolitan University, Hachioji, December 1st, 2019.
- A computational interpretation of bilateral classical logic (Joint work with Ukyo Suzuki). 科学基礎論学会 2019年度 秋の研究例会, Nihon University, Setagaya-ku, November 30th, 2019.
- Call-by-name, call-by-value, and the modal linear $\lambda$-calculus. SLACS (記号論理と情報科学研究集会) 2019, Kyoto University, Kyoto, September 9th, 2019.
- An extended SECD machine with a first-class macro mechanism. IPSJ PRO 2019-1 (情報処理学会第124回プログラミング研究発表会), Nagoya University, Nagoya, June 7th, 2019.
- On the theory and practice of program semantics by the Geometry of Interaction. Early Spring Seminar on Lambda Calculus and Logic (ラムダ計算と論理の早春セミナー), Agatsuma, March 10th, 2019.
- A Linear-logical Reconstruction of Intuitionistic Modal Logic S4 (Joint work with Akira Yoshimizu). The 53rd MLG meeting (数理論理学研究集会), Shizuoka University, Shizuoka, November 30th, 2018.
- On a linear-logical decomposition of intuitionistic modal logic S4 (Joint work with Akira Yoshimizu). SLACS (記号論理と情報科学研究集会) 2018, Hokkaido University, Sapporo, August 8th, 2018.
- On general elimination rule and its computational structure. Early Spring Seminar on Lambda Calculus and Logic (ラムダ計算と論理の早春セミナー), Semboku, March 23rd, 2018.
- Toward a Geometry of Interaction for Modal Linear Logic (Joint work with Akira Yoshimizu). Proof Theory and Proving (証明論と証明活動), RIMS, Kyoto, December 26th, 2017.
- A Cut-free Higher-arity Sequent Calculus for Modal Logic S4. The 52nd MLG meeting (数理論理学研究集会), Shizuoka University, Shizuoka, December 3rd, 2017.
- A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction (Joint work with Ryosuke Igarashi). SLACS (記号論理と情報科学研究集会) 2017, Chiba Institute of Technology, Narashino, August 8th, 2017.
- On a computational interpretation of Rumfitt's bilateral natural deduction (Joint work with Ukyo Suzuki). Kyoto Philosophical Logic Workshop II, Kyoto University, Kyoto, June 19th, 2017.
- Toward the Curry–Howard Isomorphism between Symmetric $\lambda$-calculus and Bilateral Natural Deduction. PhilLogMath (論数哲, 応用哲学会第8回研究大会2016 サテライト研究会), Ochanomizu University, Bunkyo-ku, May 6th, 2016.

- On categorical semantics of intuitionistic linear logic (直観主義線型論理の圏論的意味論について). December 11th, 2018. [ pdf ]

- Homoiconic Lisp, 2019.3–. [ GitHub ]

- 2020.1: POPL 2020, a student volunteer.
- 2017.9: ICFP 2017, a student volunteer co-captain in the organizing comitee.
- 2016.9: ICFP 2016, a student volunteer co-chair in the organizing comitee.
- 2015.7: LICS/ICALP 2015, a student volunteer.

- 2019.10–2020.1: Python Programming II (Python実習2)
- 2019.4–2019.7: Python Programming I (Python実習1)
- 2018.10–2019.1: Ruby Programming II (Ruby実習2)
- 2018.4–2018.7: Ruby Programming I (Ruby実習1)
- 2017.10–2018.2: Ruby Programming II (Ruby実習2)
- 2017.4–2017.8: Ruby Programming I (Ruby実習1)

- 2018.6–2018.7: Hardware and Software Laboratory Project 3: Software (計算機科学実験及演習3: ソフトウェア)
- 2017.10–2018.1: Computation and Logic (計算と論理)
- 2016.10–2017.1: Computation and Logic (計算と論理)
- 2016.10–2017.1: Theory of Computational Complexity (計算量理論)
- 2015.10–2016.1: Computation and Logic (計算と論理)
- 2015.6–2015.7: Hardware and Software Laboratory Project 3: Software (計算機科学実験及演習3: ソフトウェア)
- 2015.4–2015.6: Hardware and Software Laboratory Project 3: Hardware (計算機科学実験及演習3: ハードウェア)

- Dec. 4th, 1991. Born in Ise city, Mie prefecture, Japan.
- Mar. 2010. Graduated from Matsusaka High School.
- Mar. 2014. Bachelor of Computer Science and Engineering, Kyoto Sangyo Univeristy.
- Bachelor's thesis: An Implementation of the Game Semantics for Limit Computable Mathematics (極限計算可能数学のゲーム意味論の実装)
- Supervisor: Prof. Satoshi Kobayashi

- Sep. 2016. Master of Informatics, Kyoto University.
- Master's thesis: Syntactic Specifications by Singleton Code Types (シングルトンコード型による構文的仕様記述)
- Supervisor: Prof. Atsushi Igarashi

- Oct. 2016–Present. Ph.D. candidate, Graduate School of Informatics, Kyoto University.
- Supervisor: Prof. Atsushi Igarashi

- Apr. 2017–Present. Part-time lecturer, Kyoto Computer Gakuin.

- Office: Room 225, Research Bldg No 7 (総合研究7号館), Kyoto University, Yoshida-honmachi, Sakyo-ku ward, Kyoto 606-8501, Japan.
- E-mail: yfukuda [ at ] fos.kuis.kyoto-u.ac.jp