ICFP 2018 (series) / TyDe 2018 (series) / Type-Driven Development /
Extensible Type-Directed Editing
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 interactive 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.
Thu 27 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Thu 27 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
10:20 - 12:00 | |||
10:20 25mResearch paper | Typing, Representing, and Abstracting Control: Functional Pearl TyDe Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany DOI | ||
10:45 25mResearch paper | Extensible Type-Directed Editing TyDe DOI | ||
11:10 25mResearch paper | Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming TyDe Victor Cacciari Miraldo Utrecht University, Netherlands, Alejandro Serrano Utrecht University, Netherlands DOI | ||
11:35 25mResearch paper | Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL TyDe DOI |