Yukiyoshi Kameyama's Publication

• Program Generation Meets Program Verification: A Case Study on Number-Theoretic Transform
  Masahiro Masuda, Yukiyoshi Kameyama, Science of Computer Programming, Vol. 232, Jan. 2024, 103035. Available from the journal's web site.
• Generating Programs for Polynomial Multiplication with Correctness Assurance
  Ryo Tokuda, Yukiyoshi Kameyama, Proc. of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation (PEPM 2023), pp. 27-40, Jan. 2023.
• Proceedings of the 21st ACM SIGPLAN International Conference on Generative Programming: Conference and Experiences (GPCE 2022)
  Berhnard Scholz, Yukiyoshi Kameyama (editors), ACM, Dec. 2022. ISBN 978-1-4503-9920-3
• Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform
  Masahiro Masuda, Yukiyoshi Kameyama, Proc. of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science Vol. 13215, pp. 133-151, May 2022.
• Type-safe Generation of Modules in Applicative and Generative Styles
  Yuhi Sato, Yukiyoshi Kameyama, Proc. of the 20th International Symposium on Generative Programming: Concepts & Experiences (GPCE 2021), pp. 184-196, Oct. 2021.
• FFT Program Generation for Ring LWE-Based Cryptography
  Masahiro Masuda, Yukiyoshi Kameyama, Proc. of the 16th International Workshop on Security (IWSEC 2021), Lecture Notes in Computer Science Vol. 12835, pp. 151-171, Sep. 2021.
• Reorganizing Queries with Grouping
  Rui Ohkura, Yukiyoshi Kameyama, Proc. of the 19th International Symposium on Generative Programming: Concepts & Experiences (GPCE 2020), pp. 50-62, Nov. 2020.
• Language-Integrated Query with Nested Data Structures and Grouping
  Rui Ohkura, Yukiyoshi Kameyama, Proc. of the 15th International Symposium on Functional and Logic Programming (FLOPS 2020), Lecture Notes in Computer Science Vol. 12073, pp. 139-158, Sep. 2020.
• One-Shot Algebraic Effects as Coroutines
  Satoru Kawahara, Yukiyoshi Kameyama, Proc. of the 21st International Symposium on Trends in Functional Programming (TFP 2020), Lecture Notes in Computer Science Vol. 12222, pp. 159-179, Feb. 2020.
• Module Generation without Regret
  Yuhi Sato, Yukiyoshi Kameyama, Takahisa Watanabe, Proc. of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 20), pp. 1-13, Jan., 2020.
• Program Generation for ML Modules (Short Paper)
  Takahisa Watanabe, Yukiyoshi Kameyama, Proc. of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018), pp. 60-66, Jan., 2018.
• Staging with Control: Type-Safe Multi-stage Programming with Control Operators
  Junpei Oishi, Yukiyoshi Kameyama, Proc. of the 16th International Conference on Generative Programming: Concepts & Experience (GPCE 2017), pp 29-40, Vancouver, Canada, Oct. 2017.
• Refined Environment Classifiers: Type- and Scope-Safe Code Generation,
  Ole Kiselyov, Yukiyoshi Kameyama, Yuto Sudo, Proc. 14th Asian Symposium on Programming Languages and Systems (APLAS 2016), Hanoi, Vietnam, Lecture Notes in Computer Science Vol. 10017, pp. 271-291, Nov. 2016.
• Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators,
  Ikuo Kobori, Yukiyoshi Kameyama, Oleg Kiselyov, Post-Conference Proceedings of Workshop on Continuations 2015 (WoC'15), EPTCS Vol. 212, pp. 36-52, 2016.
• Proceedings of the 5th International Workshop on Functional High-Performance Computing (FHPC@ICFP 2016),
  David Duke, Yukiyoshi Kameyama (editors), Nara, Japan, Sep., 2016.
• Automatic Staging via Partial Evaluation Techniques,
  Kenichi Asai, Yukiyoshi Kameyama, Proceedings of 7th International Symposium on Symbolic Computatoin in Software Science (SCSS 2016), EPiC Series in Computing Vol. 39,pp. 1-13, Mar. 2016.
• Finally, Safely-extensible and Efficient Language-integrated Query
  Kenichi Suzuki, Oleg Kiselyov, Yukiyoshi Kameyama, ACM SIGPLAN 2016 Workshop on Partial Evaluation and Program Manipulation (PEPM'16), pp.37-48, Jan., 2016.
• Staging Beyond Terms: Prospects and Challenges
  Jun Inoue, Oleg Kiselyov, Yukiyoshi Kameyama, ACM SIGPLAN 2016 Workshop on Partial Evaluation and Program Manipulation (PEPM'16), pp.103-108, Jan., 2016.
• Combinators for Impure yet Hygienic Code Generation (link to final online version), author version
  Yukiyoshi Kameyama, Oleg Kiselyov and Chung-chieh Shan, Science of Computer Programming, Vol. 112, pp. 120-144, Nov. 2015.
• Generate and Offshore: Type-safe and Modular Code Generation for Low-Level Optimization,
  Naoki Takashima, Hiroki Sakamoto, Yukiyoshi Kameyama, Workshop on Functional High-Performance Computing (FHPC'15), 9 pages, 2015.
• Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators,
  Ikuo Kobori, Yukiyoshi Kameyama, Oleg Kiselyov, Pre-Proceedings of 2015 Workshop on Continuations (WoC'15), 12pages, Department of Computer Science, Aarhus University, April, 2015.
• Combinators for Impure yet Hygienic Code Generation
  Yukiyoshi Kameyama, Oleg Kiselyov and Chung-chieh Shan, ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM'14), San Diego, USA, Jan., 2014.
• Shonan Challenge for Generative Programming
  Baris Aktemur, Yukiyoshi Kameyama, Oleg Kiselyov and Chung-chieh Shan, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM'13), Rome, Italy, Jan., 2013.
• Lazy Delimited Nondeterminism
  Sebastian Fischer, Michael Hanus, Yukiyoshi Kameyama, Chung-chieh Shan, Naoki Takashima, International Workshop on Function and (Constraint) Logic Programming (WFLP 2012), Work-in-Progress session, Nagoya, Japan, May, 2012.
• A Call-by-Name CPS Hierarchy
  Asami Tanaka and Yukiyoshi Kameyama, Proc. International Symposium on Functional and Logic Programming (FLOPS 2012), Kobe, Japan, Lecture Notes in Computer Science Vol. 7294, pp. 260-274, May, 2012.
• Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras
  Jefferson O. Andrade, Yukiyoshi Kameyama, Special Section on Formal Approach, IEICE Transactions on Information and Systems, Vol. E95-D, No. 5, pp. 1355-1364, May, 2012. (Copyright 2012 IEICE, link to IEICE Transactions Online)
• Shifting the Stage -- Staging with Delimited Control
  Yukiyoshi Kameyama, Oleg Kiselyov, Chung-chieh Shan, Journal of Functional Programming, 21(6), pp. 617-662, 2011.
• Polymorphic Multi-Stage Language with Control Effects
  Yuichiro Kokaji, Yukiyoshi Kameyama, Proc. Ninth Asian Symposium on Programming Languages and Systems (APLAS 2011), Kenting, Taiwan, Lecture Notes in Computer Science Vol. 7078, pp. 105-120, Dec. 2011.
• Visualizing Continuations (short talk)
  Naoki Takashima, Tatsuya Nishiyama, Yukiyoshi Kameyama, ACM SIGPLAN Continuation Workshop, Tokyo, Japan, 2011.
• Undecidability of Type-checking in Domain-free Typed Lambda-Calculi with Existence
  Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano, Theoretical Computer Science, 412, pp. 6193-6207, 2011.
• Equational Axiomatization of Call-by-Name Delimited Control
  Yukiyoshi Kameyama, Asami Tanaka, Proc. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010), Hagenberg, Austria, pp. 77-86, Jul. 2010.
• Shifting the Stage: Staging with Delimited Control
  Yukiyoshi Kameyama, Oleg Kiselyov, Chung-chieh Shan, Proc. ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation (PEPM'09), Savannah, Georgia, USA, pp. 111-120, Jan. 2009.
• A Direct Algorithm for Multi-Valued Bounded Model Checking
  Jefferson O. Andrade and Yukiyoshi Kameyama, Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA 2008), Seoul, Korea, Lecture Notes in Computer Science Vol. 5311, pp. 80-94, Oct. 2008.
• Undecidability of Type-checking in Domain-free Typed Lambda-Calculi with Existence,
  Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano, Proc. Annual Conference on Computer Science Logic (CSL 2008), Lecture Notes in Computer Science Vol. 5213, pp. 478-492, Sep. 2008. (link to pdf)
• Strong Normalization of Polymorphic Calculus for Delimited Continuations
  Yukiyoshi Kameyama and Kenichi Asai, Proc. Symbolic Computation in Software Science (SCSS 2008), RISC-Linz Report Series No. 08-08, pp. 96-108, Hagenberg, Austria, July. 2008.
• Typed Dynamic Control Operators for Delimited Continuations,
  Yukiyoshi Kameyama and Takuo Yonezawa, Proc. International Symposium on Functional and Logic Programming (FLOPS 2008), Ise, Japan, Lecture Notes in Computer Science Vol. 4989, pp. 239-254, Apr. 2008.
• Calculi of Meta-Variables
  Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, and Atsushi Igarashi, Frontiers of Computer Science in China, Higher Education Press and Springer, Vol. 2, No. 1, pp. 12-21, Mar. 2008. (Journal version of CSL'03 paper: "Calculi of Meta-Variables".)
• Closing the Stage: From Staged Code to Typed Closures
  Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan, Proc. ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'08), pp. 147-157, Jan. 2008.
• A Type System for Dynamic Delimited Continuations
  Takuo Yonezawa and Yukiyoshi Kameyama, IPSJ Transaction on Programming, Information Processing Society of Japan, Vol. 49, No. SIG 3 (PRO 36), pp. 28-38, 2008. (also in IPSJ Digital Courier, Vol. 4, pp. 182-192, Mar. 2008.)
• Polymorphic Delimited Continuations
  Kenichi Asai and Yukiyoshi Kameyama, Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS 2007), Singapore, Lecture Notes in Computer Science Vol. 4807, pp. 239-254, Nov.-Dec., 2007.
• Axioms for Control Operators in the CPS Hierarchy
  Yukiyoshi Kameyama, Higher-Order and Symbolic Computation, Vol. 20, pp. 339-369, 2007.
• Simulations of Multi-Valued Models for Modal $\mu$-Calculus
  Koki Nishizawa, Yukiyoshi Kameyama, Yoshiki Kinoshita, Programming Science Technical Report AIST01-J00022-68, National Institute of Advanced Industrial Science and Technology (AIST), Japan, 18 pages, April, 2007.
• Construction of a Type System for Layered Control Operators
  Terunobu Suzuki and Yukiyoshi Kameyama, Transaction on Programming Vol. 48, No. SIG 10 (PRO 33), pp. 138-150, Information Processing Society of Japan, 2007 (in Japanese).
  [pdf in Japanese, abstract in English]
• E-learning of Foundation of Computer Science
  Yukiyoshi Kameyama, Masahiko Sato, Proc. AEARU Workshop on Network Education (AWNE2006), pp. 169-181, Taipei, Nov. 2006.
• Axioms for Delimited Continuations in the CPS Hierarchy
  Yukiyoshi Kameyama, Proc. Annual Conference of the European Association for Computer Science Logic (CSL'04), Karpacz, Poland, Lecture Notes in Computer Science 3210, pp. 442-457, Sep. 2004.
• Axiomatizing Higher Level Delimited Continuation
  Yukiyoshi Kameyama, Proc. Fourth ACM-SIGPLAN Continuation Workshop (CW'04), Venice, Italy, pp. 49-53, Jan. 2004.
• A Sound and Complete Axiomatization of Delimited Continuations
  Yukiyoshi Kameyama and Masahito Hasegawa, Proc. Eighth ACM International Conference on Functional Programming (ICFP '03), pp. 177-188, 2003.
• Calculi of Meta-Variables
  Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, and Atsushi Igarashi, Computer Science Logic (CSL '03), Lecture Notes in Computer Science 2803, pp. 484-497, 2003.
  [ps] [pdf]
• Strong Normalizability of the Catch/Throw Calculi
  Yukiyoshi Kameyama and Masahiko Sato, Theoretical Computer Science 272 (1-2), pp. 223-245, 2002.
  [ps]
• Dynamic Control Operators in Type Theory
  Yukiyoshi Kameyama, Informal Proc. Asian Workshop on Programming Languages and Systems, Daejon, Korea, Dec. 2001.
  [ps]
• Towards Logical Understanding of Delimited Continuations
  Yukiyoshi Kameyama, Proc. Third ACM Workshop on Continuations (CW'01), London, pp. 27--33, Jan. 2001.
  [ps]
• A Type-theoretic Study on Partial Continuations
  Yukiyoshi Kameyama, Proc. IFIP International Conference on Theoretical Computer Science (IFIP TCS2000), Sendai, Japan, Lecture Notes in Computer Science Vol. 1872, Aug. 2000.
  [ps]
• A Type System for Delimited Continuations
  Yukiyoshi Kameyama, Proc. JSSST Workshop on Programming and Programming Languages (PPL '2000), Kanzanji, Japan, pp. 4-11, Mar. 2000.
• A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability
  Yukiyoshi Kameyama and Masahiko Sato, Proc. CATS'98, Australian Computer Science Communications, 20(3), Springer, pp. 183-197, 1998.
  [ps]
• A Simply Typed Context Calculus with First-Class Environments
  Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama, Journal of Functional and Logic Programming 2002(4), pp. 1-41, 2002, Vol. 2002.
  [ Journal page (free)]
• A Second Order Context Calculus
  Azza A. Taha, Masahiko Sato, Yukiyoshi Kameyama, Computer Software (Journal of Japan Society of Software Science and Technology), Vol. 19, No. 3, pp. 2-19, 2002.
• CAL: A Computer Assisted Learning system for Computation and Logic
  Masahiko Sato, Yukiyoshi Kameyama, Takeuti Izumi, 8th International Workshop on Computer Aided Systems Theory (EUROCAST 2001), Lecture Notes in Computer Science Vol. 2178, pp. 509-524, 2002.
  [ps]
• A Second Order Context Calculus
  Azza A. Taha, Masahiko Sato, Yukiyoshi Kameyama, Proc. JSSST Workshop on Programming and Programming Languages (PPL 2001), Kameoka, Japan, pp. 71-82, Mar, 2001.
• A Simply Typed Context Calculus with First-Class Environments
  Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama, Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS 2001), Tokyo, Japan, Lecture Notes in Computer Science Vol. 2024, pp. 359--374, 2001.
  [ full version in ps]
  Warning: In the proceedings version (LNCS2024), there are several publisher's printing errors. For instance, all the squares (which should indicate "the end of proof") were erroneously shown as "2". Please download the journal version (see above).
• A Type-Free Context Calculus
  Azza A. Taha, Masahiko Sato, Yukiyoshi Kameyama, Journal of Information Processing Society, Japan, Vol. 42, No. 1, 2001.
• A New Formulation of the Catch/Throw Mechanism
  Yukiyoshi Kameyama, Proc. Second Fuji International Workshop on Functional and Logic Programming, Shonan Village, Nov. 1996 World-Scientific, published in 1997.
  [ps]
• A Type-Free Theory of Half-Monotone Inductive Definitions
  Yukiyoshi Kameyama, International Journal of Foundations of Computer Science, Vol. 6, No. 3 (1995), pp. 203-234.
  [ps]
• Reflective Proof Theory and its Implementation
  Yukiyoshi Kameyama and Masahiko Sato, Computer Software, Vol. 12, No. 2, pp. 32-51, 1995 (in Japanese).
  [ps in Japanese]
• Conservativeness of $\Lambda$ over $\lambda\sigma$-calculus
  Masahiko Sato and Yukiyoshi Kameyama, Logic, Language and Computation, Lecture Notes in Computer Science Vol. 792 (N. D. Jones, M. Hagiya, and M. Sato eds.) pp. 73-94, 1994.
  [ps]

Book Edition

• Functional and Logic Programming
  Yukiyoshi Kameyama, Peter J. Stuckey (eds.), Proceedings of the Seventh International Symposium on Functional and Logic Programming (FLOPS 2004), Nara, Japan, Lecture Notes in Computer Science Vol. 2998, Springer, 307 pages, 2004.

Thesis

• Reflection Mechanism in Constructive Programming
  Yukiyoshi Kameyama, PhD Thesis (Supervisor: Masahiko Sato), Kyoto University, 1996.
  [Abstract] (The thesis is available on request; send an e-mail to me.)