Return to Planet Cedille

*** PLEASE NOTE THAT WE ARE MEETING ON SUNDAY, NOT SATURDAY ***

We've looked at the Cedille language before, This time let's take a look at Cedille 2, as described in Chapter 1 of Andrew Marmaduke's thesis A proof theoretic redesign of the calculus of
dependent Lambda eliminations (https://iro.uiowa.edu/esploro/outputs/doctoral/A-proof-theoretic-redesign-of-the/9984697941302771). If you'd like to sing along, you can play with Ryan Brewer's implementation (using a different syntax) at https://ryanbrewer.dev/demos.

We'll meet over Zoom and post the meeting URL here a few minutes before meeting start time.