Dependently Typed Binary Lambda Calculus This is an implementation of a modification of Binary Lambda Calculus which adds dependent types. See here for more information. Authors Anthony Hart