README.md

Cedille Cast

The Cedille Cast is a series of videos on YouTube that covers programming and proving in Cedille, a dependently typed programming language and proof assistant. This repository contains the source files and scripts for these videos.

For more information on Cedille, check out our website.

Layout

• screencasts: directory of source files and scripts
• lib: small library of common definitions used in the casts
• .cedille: Cedille options file (local file picked over one in user's home directory)

Screencasts

• Deriving induction for lambda-encoded datatypes
  • for Church encoded naturals (parts 1 and 2)
  • generically for Mendler-syle encodings (parts 1, 2, and 3)
• Zero-cost coercions and their applications
  • Cedille's equality type and defining zero-cost coercions
  • Deriving recursive types
• Cedille features
  • Inductive datatypes in version 1.1.0
  • Interactive theorem proving in the beta-reduction buffer
• Impredicativity and proof irrelevance