Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Thu 27 Sep 2018 10:45 - 11:10 at New York Central - Types Chair(s): Richard A. Eisenberg

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 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:20 - 12:00
TypesTyDe at New York Central
Chair(s): Richard A. Eisenberg Bryn Mawr College, USA
10:20
25m
Research 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
25m
Research paper
Extensible Type-Directed Editing
TyDe
Joomy Korkut Wesleyan University, USA, David Thrane Christiansen Galois, USA
DOI
11:10
25m
Research 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
25m
Research paper
Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL
TyDe
Ilya Yanok USI Lugano, Switzerland, Nate Nystrom USI Lugano, Switzerland
DOI