This tutorial presents Cedille, a new dependently typed programming and proving language, broadly similar to tools like Coq, Agda, Lean, Idris and others. The main difference is that Cedille uses lambda encodings for all datatypes; indeed, the term language of Cedille is pure lambda calculus, without primitive datatype constructors, pattern matching, or recursion. This makes the core type theory of Cedille very minimalistic. The tutorial will present and motivate the type theory of Cedille. We will then see how to derive inductive datatypes within the theory from more primitive constructs, using impredicative type quantification but with several twists to support dependent elimination of lambda-encoded data. We will look first at basic types like the natural numbers and homogeneous lists, and then consider generic derivations of induction for any monotone type scheme. Finally, we will see how familiar datatype notations like pattern-matching recursion are supported in Cedille by opaque translation to lambda encodings. Tutorial participants will gain experience using the Cedille emacs mode, which provides a rich interactive development environment for Cedille typing.

The tutorial will use the recently released 1.0.0 version of Cedille, available at http://cedille.github.io