Language-based Security
Vorlesungen
Die Vorlesung gibt eine Einführung in den Bereich der Language-based Security.
Im github-Projekt gibt es die Coq-Quelldateien aus der Vorlesung.
1. Vorlesung
Inhalte des Abschnitts Data and Functions des Buchs Software Foundations - Volume 1.
2. Vorlesung
Inhalte der Abschnitte Proof by Simplification, Proof by Rewriting, Proof by Case Analysis und Proof by Induction des Buchs Software Foundations - Volume 1.
Abschnitt 3.1 Introduction aus dem Kapitel 3 Untyped Arithmetic Expressions aus dem Buch Types and Programming Languages.
3. Vorlesung
Inhalte der Abschnitte The apply Tactic und The apply … with … Tactic des Buchs Software Foundations - Volume 1.
Abschnitt 3.3 Induction on Terms aus dem Kapitel 3 Untyped Arithmetic Expressions aus dem Buch Types and Programming Languages.
4. Vorlesung
Inhalte der Abschnitte Inductively Defined Propositions, Using Evidence in Proofs und Inductive Relations des Buchs Software Foundations - Volume 1.
Abschnitt 3.5 Evaluation aus dem Kapitel 3 Untyped Arithmetic Expressions aus dem Buch Types and Programming Languages.
5. Vorlesung
Inhalte der Abschnitte Relations, Basic Properties und Reflexive, Transitive Closure des Buchs Software Foundations - Volume 1.
Abschnitt 3.4 Semantic Styles aus dem Kapitel 3 Untyped Arithmetic Expressions aus dem Buch Types and Programming Languages.
6. Vorlesung
Inhalte des Abschnitts Varying the Induction Hypothesis des Buchs Software Foundations - Volume 1.
Kapitel 8 Typed Arithmetic Expressions aus dem Buch Types and Programming Languages.
7. Vorlesung
Inhalte des Abschnitts The eapply and eauto variants des Buchs Software Foundations - Volume 1.
8. Vorlesung
Abschnitt 4.1 des Kapitels Typed Assembly Language aus dem Buch Advanced Topics in Types and Programming Languages.
9. Vorlesung
Wiederholung Abschnitt 4.1 des Kapitels Typed Assembly Language aus dem Buch Advanced Topics in Types and Programming Languages.
Funktionale Programmierung in der Industrie
Verwendung von Coq in der Forschung
- Die wisenschaftliche Arbeit Formal verification of a realistic compiler stellt einen mit Coq verifizierten C-Compiler vor
- Die Liste der Coq-Repositories bei github gibt einen guten Eindruck über die Verwendung von Coq