David Christiansen


  • Office: 130 in Lindley Hall

  • Work: davidchr at indiana dot edu

  • Personal: david at davidchristiansen dot dk

  • IRC: christiansen on Freenode

I build systems that enable programming to be a creative dialog between human and machine. To do this, I work with advanced type systems, metaprogramming, and domain-specific languages. In particular, I’ve written a fair bit of Idris.

I’m a postdoc at Indiana University in Bloomington, IN, USA. I completed my Ph.D. at the IT University of Copenhagen, Denmark, in January 2016 under the supervision of Peter Sestoft.


Elaborator Reflection: Extending Idris in Idris (pdf, acm, video)
David Christiansen, Edwin Brady
In Proc. of 21st International Conference on Functional Programming (ICFP ’16)
Nara, Japan, September, 2016
Making the elaboration facilities available for metaprogramming in Idris.

Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection (pdf, acm)
David Raymond Christiansen
In Proc. of 26th International Symposium on Implementation and Application of Functional Languages (IFL ’14)
Boston, Massachusetts, USA, October, 2014
A means of implementing quasiquotation in the context of a type-directed tactic-driven elaborator.

Pension Reserve Computations on GPUs (pdf, acm)
Christian Harrington, Nicolai Dahl, Peter Sestoft, David Raymond Christiansen
In Proc. of Workshop on Functional High-Performance Computing (FHPC ’14)
Gothenbug, Sweden, September, 2014
A description of generation of fast GPU code for solving the Thiele’s differential equations, generated from a high-level description of a class of life insurance and pension products.

Dependent Type Providers (pdf, acm)
David Raymond Christiansen
In Proc. of Workshop on Generic Programming (WGP ’13)
Boston, Massachusetts, USA, September, 2013
A mechanism for allowing datatype indices to be about something outside the language

Banana Algebra: Compositional Syntactic Language Extension (pdf)
Jacob Andersen, Claus Brabrand, David Raymond Christiansen
In Science of Computer Programming, Vol. 78(10), Elsevier, 2013

Software Development for the Working Actuary (pdf, poster)
David Raymond Christiansen
In Proc. of 4th International Symposium on End-User Development (IS-EUD ’13)
Copenhagen, Denmark, June, 2013
A short paper describing ongoing research and associated poster

Formal Semantics and Implementation of BPMN 2.0 Inclusive Gateways (pdf)
David Raymond Christiansen
In Proc. of Web Services and Formal Methods (WS-FM ’10)
Hoboken, New Jersey, USA, September, 2010


Reflect on Your Mistakes! Lightweight Domain-Specific Error Messages (pdf)
David Raymond Christiansen
Presented at TFP 2014, Soesterberg, The Netherlands, May, 2014
A mechanism for displaying error messages for embedded languages using the terms of the embedded language rather than the host language.

Selected Talks

Elaborator Reflection: Extending Idris in Idris (video)
David Christiansen
Presented at ICFP 2016

A Pretty Printer that Says What it Means (video)
David Christiansen
Presented at Haskell Implementors’ Workshop 2015

Coding for Types: The Universe Pattern in Idris (video)
David Christiansen
Presented at Curry On 2015

Type Providers and Error Reflection in Idris (video)
David Christiansen
Presented at Compose 2015

Tool Demonstration: An IDE for Programming and Proving in Idris (pdf)
Hannes Mehnert, David Christiansen
Presented at DTP 2014

An Actuarial Programming Language for Life Insurance and Pensions (pdf)
David Christiansen, Henning Niss, Klaus Grue, Kristján S. Sigtryggsson, Peter Sestoft
Presented at ICA 2014



I’m a contributor to Idris, a functional programming language with full dependent types. In particular, I’m to blame for Idris’s take on type providers, quasiquotation, and the reflected elaborator.

I am a co-author and maintainer of the Idris IDE for Emacs, which attempts to unite the interaction styles of SLIME, agda-mode, and ProofGeneral, and to be a practical environment for writing runnable code using dependent types.

My current project is Pudding, a proof assistant that is deeply integrated with the Racket programming language.

Dissertation and Thesis

I defended my Ph.D. dissertation, Practical Reflection and Metaprogramming for Dependent Types, on January 7, 2016. It describes a suite of metaprogramming features for Idris, including a means of quoting Idris’s core language using high-level Idris syntax, a way to rewrite error messages that arise from embedded languages, and a reflection of Idris’s elaborator into a monad with effects in the type checker.

My M.Sc. thesis (Danish speciale) describes Idris’s type providers, which allow dependent types to talk about values obtained from effectful computations that can observe the world in which the program finds itself being typechecked.


I’ve created some tutorials in connections with my teaching duties. In case they are useful outside of the specific courses for which they were designed, they are now online.

I’m a co-host of The Type Theory Podcast.

I’m a fluent user of English and Danish. I can also get by in Swedish and Esperanto, if necessary.