Heifer: A Type Theory for Creating Programming Languages

Date

April 28rd, 2008

Speaker

Edwin Westbrook

Abstract

This talk will introduce Heifer, a novel type theory for creating programming languages. Based on the Curry-Howard isomorphism or "propositions as types" principle, Heifer allows the user to both manipulate and prove properties of programming languages. The key difficulty is in encoding variable binding, which is known to be cumbersome to formalize in standard type theories. Heifer solves this problem by adding a construct to the type theory which gives the properties of variable binding "for free" This leads to a new encoding technique for variable binding, higher-order encodings with constructors, which is both powerful and simple.