You are here:
(02 Sep 2010,
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 -->
ore topic actions
Topic revision: r3 - 02 Sep 2010,
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?