Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 15:30 - 15:55 at Noh Theater - Session 7 Chair(s): Andres Löh

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris's reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.

Tue 20 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

15:05 - 16:20
Session 7Research Papers at Noh Theater
Chair(s): Andres Löh Well-Typed LLP
15:05
25m
Talk
Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Research Papers
Jesper Cockx iMinds, Belgium, Dominique Devriese iMinds, Belgium, Frank Piessens iMinds, Belgium
DOI
15:30
25m
Talk
Elaborator Reflection: Extending Idris in Idris
Research Papers
David Thrane Christiansen Indiana University, USA, Edwin Brady University of St. Andrews, UK
DOI
15:55
25m
Talk
Partial Type Equivalences for Verified Dependent Interoperability
Research Papers
Pierre-Evariste Dagand UPMC, France, Nicolas Tabareau Inria, France, Éric Tanter University of Chile, Chile
DOI