A dependently-typed programming language and interactive theorem prover with an extrinsic type system based on the untyped lambda calculus.