Home
Schedule
Abstract Template
Masters Attendance
Implementing ADependently Typed Lambda Calculus

Stc
Date: 2007-04-12 

Time: 11:45

Room: BBL room 471

----+++ Speaker: Wouter Swierstra (University of Nottingham)

----+++ Title: Implementing a Dependently Typed Lambda Calculus

----+++ Abstract


Most Haskell programmers know how to implement a type checker for the  
simply typed lambda calculus. Quite a few know how to implement  
Hindley-Milner style type inference. When it comes to implementing a  
dependently typed calculus, however, most people don't even know  
where to start. Based on experience with Epigram, I hope to show how  
to implement the most rudimentary core of a dependently typed  
programming language. Surprisingly, the implementation is no more  
difficult than that for the simply typed lambda calculus.

Note: I'll not assume any prior knowledge about dependent types,  
though it might help if you have some experience with turning  
inference rules into Haskell code. This is joint work with Conor  
<nop>McBride and Andres Loeh.

<!--
   * Set PREV_SKIN = customtitle
   * Set CUSTOMTOPICTITLE = Implementing a Dependently Typed Lambda Calculus
   * Set CUSTOMHEADTITLE = Stc / Implementing a Dependently Typed Lambda Calculus
-->