Typcheck-Schlussregeln in einer einfachen / abhängig typisierten Programmiersprache
Der Slogan "Well-typed programs don't go wrong" mit den Statements vom Progress und Preservation-Lemma (siehe hier). Vielleicht kriegen wir ja sogar Beweisskizzen unter!
die Curry-Howard-Korrespondenz anhand von Beispielen
"Viele" Leute sind ja Fans von laminierten Pi-Kärtchen: http://rawgit.com/iblech/mathezirkel-kurs/master/mathecamp-2014/pi-lernen/pi-lernen.pdf
Wir sollten ein Analogon für den Curry Club erstellen, auch zur Verteilung auf dem Kongress. Können wir auf diesem Issue Vorschläge sammeln?