Research theme for competitive and other funds (35)：
2022 - 2026 Theory and Implementation of Dependently Typed Staged Computation
2018 - 2022 Staged Computing based on Advanced Type Systems
2017 - 2021 クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化
2015 - 2018 Design and development of multi-stage languages for verification
2013 - 2016 Study on Highly Reliable Programming Languages for Code Generation
2013 - 2015 Calculi for Call-by-Need and Control Abstraction
2011 - 2012 Logical aspect of Control Operators and Program Extraction
2009 - 2012 Foundation of Programming Languages for Code Generation
2008 - 2009 多値モデル検査法を用いたモデリング・エラーの発見
2006 - 2009 Foundation and Application of Delimited Continuations
2007 - 2008 Study on Semantics and Abstraction Methods based on Multi-Valued Kripke Structures
2005 - 2008 Study on Automatic Program Generation and its Reliability
2004 - 2007 Foundation of Meta-Programming
2006 - 2006 安全・安心な環境適応型ソフトウェアの基礎理論に関する研究
2004 - 2005 変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
2001 - 2005 Study on Meta-level primitives in Programming Languages
2003 - 2003 変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
2001 - 2003 Calculus and Logic of Delimited Continuations
2001 - 2003 Calculi and Logic of Environment and Context
1998 - 2001 Research and Developement of Computer-Aided Education System for Logic and Computation
1998 - 2001 Study on Data Refinement in Program Verification
2001 - Programming Logic
2001 - Software Verification
1999 - 2000 コントロール・オペレータの計算系とプログラム合成
1998 - 1999 Implementation of Constructive Programming Based on Classical Logic
1997 - 1998 構成的プログラミングの手法による制御機構を持つプログラムの合成
1996 - 1997 Design and Implementation of Constructive Programming Systems
1996 - 1997 Theory of Constructive Programming
1996 - 1996 構成的プログラミングにおける非局所脱出機構を持つプログラムの合成
1995 - 1995 自己反映原理を応用した構成的プログラミング
1994 - 1995 Constructive Programming System for Proof Development, Verification, and Program Synthesis
1993 - 1995 Research on advanced application technology of large-scale internets and Open distributed processing
1993 - 1993 構成的論理体系における仕様記述と証明作成に関する研究
1990 - 1992 Co-operative research on foundational theories of programs
1987 - 1989 Design of Proving, Verifying, and Synthesizing System based on Constructive
Show all
Papers (140)：
Masuda, Masahiro, Kameyama, Yukiyoshi. Program generation meets program verification: A case study on number-theoretic transform. SCIENCE OF COMPUTER PROGRAMMING. 2024. 232
Tokuda, Ryo, Kameyama, Yukiyoshi. Generating Programs for Polynomial Multiplication with Correctness Assurance. Proceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation. 2023. 27-40
Masahiro Masuda, Yukiyoshi Kameyama. Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform. Proceedigs of the 16th Internatioal Symposium on Functional and Logic Programming (FLOPS 2022), Springer LNCS. 2022. 13215. 133-151
Yuhi Sato, Yukiyoshi Kameyama. Type-safe generation of modules in applicative and generative styles. Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. 2021. 184-196
Proceedings of the 5th International Workshop on Functional High-Performance Computing
ACM 2016 ISBN:9781450344333
PEPM'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN SYMPOSIUM ON PARTIAL EVALUATION AND SEMANTICS-BASED PROGRAM MANIPULATION
ASSOC COMPUTING MACHINERY 2008 ISBN:9781595939777
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS
SPRINGER-VERLAG BERLIN 2008 ISBN:9783540883869
FUNCTIONAL AND LOGIC PROGRAMMING
SPRINGER-VERLAG BERLIN 2008 ISBN:9783540789680
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS
SPRINGER-VERLAG BERLIN 2007 ISBN:9783540766360
Generating Programs for Polynomial Multiplication with Correctness Assurance
(The 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation)
代数的エフェクトを持つ2段階計算言語の型システム
(日本ソフトウェア科学会第39回大会)
Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform
(The 16th International Symposium on Functional and Logic Programming 2022)
