Welcome to Kenichi Asai's Home Page

Home

Publications

• English
• Japanese (PPL)

Projects

• Type Debugger
• Universe Library
• OchaCaml
• MikiBeta
• Meta Lambda Calculus
• Black

Address

2023

• Cong, Y., and K. Asai "Towards a Reflection for Effect Handlers," ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '23), pp. 55-65 (January 2023). ACM DL.
  
  

2022

• Ishio, C., and K. Asai "Type System for Four Delimited Control Operators," Proceedings of the 21st ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2022), pp. 45-58 (December 2022). Received Best Paper Award. ACM DL.
  
  
• Cong, Y., C. Ishio, K. Honda, and K. Asai "A Functional Abstraction of Typed Invocation Contexts," Logical Methods in Computer Science, Vol. 18, Issue 3, 31 pages (September, 2022). abstract, pdf, formalization in Agda.
  
  
• Cong, Y., and K. Asai "Towards Dependently-Typed Control Effects (Extended Abstract)," The 7th Workshop on Type-Driven Development (TyDe 2022), Ljubljana, Slovenia, 5 pages (September 2022).
  
  
• Cong, Y., and K. Asai, "Understanding Algebraic Effect Handlers via Delimited Control Operators," In W. Swierstra and N. Wu editors, Trends in Functional Programming (TFP 2022) (March 2022). Post conference version in LNCS 13401, pp. 59-79 (January 2023).
  
  

2021

• Cong, Y., C. Ishio, K. Honda, and K. Asai "A Functional Abstraction of Typed Invocation Contexts," 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), 18 pages (July 2021). abstract, pdf, formalization in Agda.
  
  
• Fujii, M., and K. Asai "Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators," 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), 19 pages (July 2021). abstract, pdf, source code, github.
  
  
• Asai, K., Y. Cong, and C. Ishio "A Functional Abstraction of Typed Trails," ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '21), 7 pages (January 2021). abstract, pdf, formalization in Agda.
  
  

2019

• Ishio, C., and K. Asai, "Verifying Selective CPS Transformation for Shift and Reset," In W. Bowman and R. Garcia editors, Trends in Functional Programming (TFP 2019), LNCS 12053, pp. 38-57 (May 2020), formalization in Agda.
  
  
• Furukawa, T., Y. Cong, and K. Asai, "Stepping OCaml," Trends in Functional Programming in Education (June 2018). Post proceedings version in Electronic Proceedings in Theoretical Computer Science 295, pp. 17-34 (June 2019).
  
  
• Asai, K. "Extracting a Call-by-Name Partial Evaluator from a Proof of Termination," ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '19), pp. 61-67 (January 2019). abstract, ACM DL, formalization in Agda.
  
  

2018

• Yamada, U., and K. Asai "Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS," In S. Ryu editor, 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), LNCS 11275, pp. 375-393 (December 2018). abstract, formalization in Agda.
  
  
• Cong, Y., and K. Asai "Handling Delimited Continuations with Dependent Types," Proceedings of the ACM on Programming Languages, Vol. 2, Issue ICFP, Article 69, 31 pages (September 2018). abstract, ACM DL.
  
  
• Asai, K., and C. Uehara "Selective CPS Transformation for Shift and Reset," ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '18), pp. 40-52 (January 2018). Received Best Paper Award. abstract, ACM DL.
  
  

2017

• Asai, K. "Delimited Continuations for Everyone," Papers We Love Conference, St. Louis, MO (September 2017). slides.
  
  

2016

• Asai, K. "Principle and Practice of OCaml Type Debugger," ACM SIGPLAN Programming Languages Mentoring Workshop at ICFP, Nara Japan (September 2016). abstract, slides, video.
  
  
• Asai, K., and K. Kadowaki "A Type Theoretic Specification of Type Inference," preprint (July 2016). pdf, agda.
  
  
• Asai, K., and Y. Kameyama "Automatic Staging via Partial Evaluation Techniques," In J. H. Davenport and F. Ghourabi editors, 7th International Symposium on Symbolic Computation in Software Science (SCSS '16), EPiC Series in Computing, Vol. 39, pp. 1-13 (March 2016). EPiC.
  
  
• Cong, Y., and K. Asai "Implementing a stepper using delimited continuations," In J. H. Davenport and F. Ghourabi editors, 7th International Symposium on Symbolic Computation in Software Science (SCSS '16), EPiC Series in Computing, Vol. 39, pp. 42-54 (March 2016). EPiC.
  
  
• Asai, K. "Toward Introducing Binding-Time Analysis to MetaOCaml," ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '16), pp. 97-102 (January 2016). abstract, ACM DL.
  
  

2015

• Uehara, C., and K. Asai "Cross validation of the universe teachpack of Racket in OCaml," 4th International Workshop on Trends in Functional Programming in Education, 14 pages (June 2015). pdf.
  
  

2014

• Asai, K. "Compiling a Reflective Language using MetaOCaml," Proceedings of the 2014 International Conference on Generative Programming: Concepts and Experiences (GPCE '14), pp. 113-122, Vasteras, Sweden (September 2014). abstract, ACM DL.
  
  
• Asai, K., L. Fennell, P. Thiemann, and Y. Zhang "A Type Theoretic Specification of Partial Evaluation," Proceedings of the 2014 Symposium on Principles and Practice of Declarative Programming (PPDP '14), pp. 57-68 (September 2014). abstract, ACM DL.
  
  
• Ishii, Y., and K. Asai "Report on a User Test and Extension of a Type Debugger for Novice Programmers," 3rd International Workshop on Trends in Functional Programming in Education, 14 pages (June 2014). Post proceedings version in Electronic Proceedings in Theoretical Computer Science 170, pp. 1-18 (December 2014).
  
  
• Hirota, N., and K. Asai "Formalizing a Correctness Property of a Type-Directed Partial Evaluator," Programming Languages meets Program Verification (PLPV), pp. 41-46, San Diego (January 2014). abstract, ACM DL, formalization in Coq, Agda.
  
  

2012/2013

• Tsushima, K., and K. Asai "An Embedded Type Debugger," The 24th Symposium on Implementation and Application of Functional Languages, Oxford (August 2012). abstract. Post conference version in LNCS 8241, pp. 190-206 (2013). Received Peter Landin Prize.
  
  

2011

• Asai, K., O. Kiselyov, and C.-c. Shan "Functional un|unparsing," Higher-Order and Symbolic Computation, Vol. 24, No. 4, pp. 311-340, Springer, DOI 10.1007/s10990-012-9087-2 (November 2011).
  
  
• Asai, K. "Reflection in Direct Style," Proceedings of the Tenth Conference on Generative Programming and Component Engineering (GPCE '11), pp. 97-106 (October 2011). abstract, ACM DL.
  
  
• Asai, K., and O. Kiselyov "Introduction to Programming with Shift and Reset," Tutorial in the ACM SIGPLAN Continuation Workshop (CW 2011). See the tutorial page for tutorial notes and other information (September 2011).
  
  
• Masuko, M., and K. Asai "Caml Light + shift/reset = Caml Shift," Theory and Practice of Delimited Continuations (TPDC 2011), pp. 33-46 (May 2011). abstract, pdf.
  
  
• Ueda, Y., and K. Asai "Reinvestigation of Symmetric Lambda Calculus," Proceedings of the 4th DIKU-IST Joint Workshop on Foundations of Software, Technical Report 2011/1, DIKU, University of Copenhagen, pp. 10-26 (February 2011). pdf.
  
  

2010

• Asai, K., and A. Kitani "Functional Derivation of a Virtual Machine for Delimited Continuations," Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming (PPDP '10), pp. 87-97 (July 2010). abstract, pdf, program.
  
  
• Sakurai, K., and K. Asai "MikiBeta: A General GUI Library for Visualizing Proof Trees," 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '10), pp. 184-193 (July 2010). abstract, pdf. Post conference version in LNCS 6564, pp. 84-98 (April 2011).
  
  

2009

• Bekki, D., and K. Asai "Representing Covert Movements by Delimited Continuations," Proceedings of the Sixth International Workshop on Logic and Engineering of Natural Language Semantics (LENLS 6), pp. 71-90 (November 2009). New Frontiers in Artificial Intelligence, LNAI 6284, pp. 161-180 (2010).
  
  
• Masuko, M., and K. Asai "Direct Implementation of Shift and Reset in the MinCaml Compiler," Proceedings of the 2009 ACM SIGPLAN Workshop on ML, pp. 49-60 (September 2009). Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 09-1, 27 pages (May 2009). abstract, cover page, pdf.
  
  
• Kitani, A., and K. Asai "Derivation of an Abstract Machine for lambda-calculus with Delimited Continuation Constructs," Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 08-3, 25 pages (March 2009). abstract, cover page, pdf.
  
  

2008

• Asai, K. "On Typing Delimited Continuations: Three New Solutions to the Printf Problem," Higher-Order and Symbolic Computation, Vol. 22, No. 3, pp. 275-291, Springer (September 2009). Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 08-2, 17 pages (September 2008). abstract, cover page, a4.ps, pdf. (A shorter version is available as OCHA-IS 07-1. See below.)
  
  
• Kameyama, Y. and K. Asai "Strong Normalizatoin of Polymorphic Calculus for Delimited Continuations," Austrian-Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008), RISC-Linz Report Series No. 08-08, pp. 96-108 (July 2008). abstract, proceedings
  
  

2007

• Asai, K. and Y. Kameyama "Polymorphic Delimited Continuations," In Z. Shao editor, 5th Asian Symposium on Programming Languages and Systems (APLAS 2007), LNCS 4807, pp. 239-254 (November 2007). abstract, slides. An extended version with proofs is available as Technical Report of Department of Computer Science, University of Tsukuba, CS-TR-07-10, 22 pages, (November 2007).
  
  
• Asai, K. "On Typing Delimited Continuations: Three New Solutions to the Printf Problem," Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 07-1, 9 pages (September 2007). abstract, cover page, a4.ps, pdf, slides presented at Continuation Fest 2008 (April 2008). The extended version with an introduction to CPS, shift and reset is available as OCHA-IS 08-2. See above.
  
  

2006

• Asai, K. "Logical Relations for Call-by-value Delimited Continuations," A chapter of Trends in Functional Programming, Vol. 6, pp. 63-78, Intellect (2007). abstract, a4.ps, pdf. An extended version appears as Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 06-1, 28 pages (April 2006). cover page, a4.ps, pdf
  
  

2005

• Asai, K. "Logical Relations for Call-by-value Delimited Continuations," Sixth Symposium on Trends in Functional Programming (TFP 2005), pp. 413-428 (September 2005). abstract, a4.ps
  
  
• Asai, K. "OCaml Course in Ochanomizu University," Presented at "Tips and Tricks" session of the ACM SIGPLAN Workshop on Functional and Declarative Programming in Education (FDPE '05), (September 2005). html
  
  

2004

• Asai, K. "Offline Partial Evaluation for Shift and Reset," ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '04), pp. 3-14 (August 2004). abstract, a4.ps
  
  

2003

• Asai, K. "Reflecting on the Metalevel Interpreter Written in Direct Style," Presented at the International Lisp Conference 2003 (ILC 2003), New York City (October 2003). abstract, a4.ps
  
  

2002

• Asai, K. "Can partial evaluation improve the performance of ray tracing?," Natural Science Report, Ochanomizu University, Vol. 53, No. 1, pp. 97-100 (June 2002). Presented at the 3rd Joint Forum of Ewha Womans U., Japan Women's U. and Ochanomizu U. for the Promotion of Education and Research in Science for Women in the 21st Century (November 2001). abstract, a4.ps
  
  
• Asai, K. "Online Partial Evaluation for Shift and Reset," ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '02), pp. 19-30 (January 2002). abstract, a4.ps
  
  

2001

• Asai, K. "Binding-Time Analysis for Both Static and Dynamic Expressions," New Generation Computing, Vol. 20, No. 1, pp. 27-51 (November 2001). abstract, a4.ps
  
  
• Asai, K. "Integrating Partial Evaluators into Interpreters," In W. Taha editor, Semantics, Applications, and Implementation of Program Generation (LNCS 2196), pp. 126-145 (September 2001). abstract, a4.ps, see LNCS 2196 for pdf
  
  

1999

• Asai, K. "Binding-Time Analysis for Both Static and Dynamic Expressions," In A. Cortesi and G. File editors, Static Analysis (LNCS 1694), pp. 117-133 (September 1999). abstract, a4.ps, see LNCS 1694 for pdf
  
  

1997

• Asai, K., H. Masuhara, and A. Yonezawa "Partial Evaluation of Call-by-value Lambda-calculus with Side-effects," ACM SIGPLAN Conference on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '97), pp. 12-21 (June 1997). ACM SIGPLAN Notices, Vol. 32, No. 12 (December 1997). abstract, a4.ps
  
  
• Asai, K. "The Reflective Language Black," Doctoral Dissertation, Department of Information Science, Graduate School of Science, University of Tokyo, 103 pages (February 1997). abstract, a4.ps
  
  

1996

• Asai, K., H. Masuhara, and A. Yonezawa "Partial Evaluation of Call-by-value lambda-calculus with Side-effects," Technical report of Department of Information Science, University of Tokyo, 96-04 (November 1996). abstract, a4.ps
  
  
• Asai, K., S. Matsuoka, and A. Yonezawa "Duplication and Partial Evaluation - For a Better Understanding of Reflective Languages -," Lisp and Symbolic Computation, Vol. 9, Nos. 2/3, pp. 203-241, Kluwer Academic Publishers (May/June 1996). abstract, a4.ps, letter.ps, program
  
  

1995

• Asai, K., H. Masuhara, S. Matsuoka, and A. Yonezawa "Partial evaluation as a compiler for reflective languages," Technical report of Department of Information Science, University of Tokyo, 95-10 (December 1995). abstract, a4.ps
  
  
• Masuhara, H., S. Matsuoka, K. Asai, and A. Yonezawa "Compiling Away the Meta-Level in Object-Oriented Concurrent Reflective Languages Using Partial Evaluation," Tenth Annual Conference of Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '95), pp. 300-315, (October 1995). ACM SIGPLAN Notices, Vol. 30, No. 10 (October 1995). See Masuhara's page.
  
  

1994

• Asai, K., S. Matsuoka, and A. Yonezawa "Roles of a Partial Evaluator for the Reflective Language Black," Technical report of Department of Information Science, University of Tokyo, 94-11 (May 1994). abstract, a4.ps, letter.ps
  
  

---

Last modified on March 12, 2024

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.