Prüfer: Daniel Gorín

  * Was macht contradiction?

  * In welchem Fall hilft kontradiction?
      - H: 0 = 1
      - H: False
      - H: A /\ ~A
  
  * 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)