Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Edwin Brady

LFCS Seminar: Edwin Brady

— filed under:

Idris: General Purpose Programming with Dependent Types

  • LFCS Seminar
When Nov 20, 2012
from 04:00 PM to 05:00 PM
Add event to calendar vCal

Idris ( is a general purpose pure functional programming
language with dependent types. Dependent types allow types to be predicated on
values, meaning that some aspects of a program’s behaviour can be specified
precisely in the type.  It is compiled, with eager evaluation. Its syntax is
influenced by Haskell, and features include full dependent types, records, type
classes, tactic based theorem proving, and an optimising compiler with a
foreign function interface.

In this talk I will introduce dependently typed programming using Idris, and
demonstrate its features using several examples including an interpreter for
the simply typed lambda calculus, and a verified binary adder.

Document Actions