Apr. 1st, 2021. This page is no longer maintained. Please refer to the new page: https://lambda.ski

Yosuke Fukuda (福田 陽介)

I'm currently working as a research specialist at STAIR Lab, Chiba Institute of Technology. I'm also a Ph.D. course student in Computer Software Group (Igarashi/Suenaga Lab), Graduate School of Informatics, Kyoto University, under the supervision of 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:

1. A geometry of interaction machine for (multi-)staged computation.
2. 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)

Publication

• 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 ]

Non-refereed Publication

• 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 ]

Poster

• 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.

Contributed Talk

• 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 ]

Non-refereed Presentation

• Extracting a formal system of typed combinators, informally. SLACS (記号論理と情報科学研究集会) 2020, December 3rd, 2020.
• On a generalization of the Curry correspondence. IPSJ PRO 2020-3 (情報処理学会第131回プログラミング研究発表会), October 30th, 2020.
• A geometry of intraction semantics for a modal λ-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 λ-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 λ-calculus and Bilateral Natural Deduction. PhilLogMath (論数哲, 応用哲学会第8回研究大会2016 サテライト研究会), Ochanomizu University, Bunkyo-ku, May 6th, 2016.

Miscellaneous Document (written in Japanese)

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

Program

• Homoiconic Lisp, 2019.3–. [ GitHub ]

Activity

Academic Activity

• 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.

Teaching at Kyoto Computer Gakuin

• 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)

Teaching Assistant at Kyoto University

• 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: ハードウェア)

Brief CV

• 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–Mar. 2020. Part-time lecturer, Kyoto Computer Gakuin.
• Apr. 2020–Present. Research specialist, STAIR Lab, Chiba Institute of Technology.

Contact

• Office: Room 212, STAIR Lab (Bldg. No. 4), Tsudanuma Campus, Chiba Institute of Technology, Tsudanuma 2-17-1, Narashino, Chiba 275-0016, Japan
• E-mail: yfukuda [ at ] stair.center
• E-mail: yfukuda [ at ] fos.kuis.kyoto-u.ac.jp