Wie ist der Existenzquantor in Coq definiert? Wie Beweist man eine existenzquantifizierte Aussage?
Was ist ein Hoare-Triple? (Im Gespräch: Keine Aussage über Terminierung)
Nenne einige Hoare-Triple!
Was sind die Sprachkonstruktre des Lambda-Kalküls? Nach etwas diskussion: Church-Style vs. Curry-Style
Wie müsste man die Semantik von Imp verändern, wenn man ein „return“ implementieren möchte, das ans Ende des Programms springt?
Wofür ist Typisierung in Imp gut? Was hat es mit type preservation auf sich? (Das Gespräch ging in Richtung „stuck“, „value“, Semantisches vs. Syntaktisches Konzept)