Language-based Security

Last changed on May 16, 2018

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