Extensible type-directed editing
Extensible type-directed editing
复制标题
可扩展的类型定向编辑
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
D. Christiansen
中科院分区：
文献类型：
--
作者：
Joomy Korkut;D. Christiansen
依赖类型的编程语言，如Idris和Agda，具有丰富的交互式环境，这些环境使用信息类型来帮助用户构建程序。然而，这些环境是由该语言的作者提供的，用户没有一种简单的方法来扩展和定制它们。我们通过使用描述新的面向类型的编辑特性的原语来扩展Idris的元编程工具来解决这个问题，使Idris的编辑器与它的阐述器一样可扩展。
Dependently typed programming languages, such as Idris and Agda, feature rich interactive environments that use informative types to assist users with the construction of programs. However, these environments have been provided by the authors of the language, and users have not had an easy way to extend and customize them. We address this problem by extending Idris's metaprogramming facilities with primitives for describing new type-directed editing features, making Idris's editors as extensible as its elaborator.
DOI：
10.1145/2951913.2951932
发表时间：
2016-09
期刊：
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
D. Christiansen;Edwin C. Brady
通讯作者：
D. Christiansen;Edwin C. Brady