Domain Specific Language Implementation with Dependent Types

These are slides from a talk at a Functional Programming Group lunchtime meeting, on October 26th 2009. It covers dependently typed programming in Idris, using Domain Specific Language implementation as an example.

You can find code at the bottom of the page.

• Examples from the talk
• The type safe interpreter
• The file DSEL
  • handle.idr, env.idr listmem.idr, support files
  • infile-big, bigdatafile, input files

Edwin Brady -- eb@cs.st-andrews.ac.uk -- 26th October 2009