CPS 変æ›ã®æ£å½“性㮠Agda ã«ã‚ˆã‚‹è¨¼æ˜Ž
石尾 åƒæ™¶ã€å±±ç”° 麗ã€æµ…井 å¥ä¸€
2018 年 3 月 6 日
PPL 2018 ã®è«–æ–‡
石尾 åƒæ™¶ã€å±±ç”° 麗ã€æµ…井 å¥ä¸€
「Agda ã«ã‚ˆã‚‹ PHOAS を用ã„㟠CPS 変æ›ã®æ£å½“性ã®è¨¼æ˜Žã€
第２ï¼å›žãƒ—ãƒã‚°ãƒ©ãƒŸãƒ³ã‚°ãŠã‚ˆã³ãƒ—ãƒã‚°ãƒ©ãƒŸãƒ³ã‚°è¨€èªžãƒ¯ãƒ¼ã‚¯ã‚·ãƒ§ãƒƒãƒ—論文集ã€
17 ページ (2018 年 3 月)。
PDF
ã§å®šå¼åŒ–ã—㟠CPS 変æ›ã®æ£å½“性ã®è¨¼æ˜Žã® Agda ファイル。
-
mono.agda
- å˜ç›¸ã®Î»è¨ˆç®—。
- poly.agda
- let 多相ã®å…¥ã£ãŸÎ»è¨ˆç®—。
This document was translated from LATEX by
HEVEA.