Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States

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

Thu 27 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 12:00
T01: Introduction to Programming and Proving in CedilleTutorials at Burlington Route
Chair(s): Aaron Stump The University of Iowa, USA
T01: Introduction to Programming and Proving in Cedille
Aaron Stump The University of Iowa, USA, Chris Jenkins The University of Iowa, Colin McDonald