| Schedule subject to change as course progresses. |
|---|
| Lecture slides for not yet given lectures are preliminary, and may change. |
|---|
| Jan 21 |
Course Introduction |
slides (full sized PDF)
(six up PDF)
files Demo1.thy
files Demo2_inc.thy
|
|---|
| Jan 23 |
Intro continued |
slides (full sized PDF)
(six up PDF)
|
|---|
| |
|---|
| Jan 28 |
Basic Isabelle syntax |
slides (revised) (full sized PDF)
(six up PDF)
|
|---|
| Jan 30 |
Introducing new types and terms |
slides (full sized PDF)
(six up PDF)
files Demo3.thy
|
|---|
| |
|---|
| Feb 4 |
Datatypes and Definitions |
slides (full sized PDF)
(six up PDF)
files Demo4.thy
|
|---|
| Feb 6 |
Rewriting Simplification |
slides (full sized PDF)
(six up PDF)
files Demo4.thy
files Demo5.thy
|
|---|
| |
|---|
| Feb 11 |
Rewriting, Introduction and Elimination Rules in HOL |
slides (full sized PDF)
(six up PDF)
|
|---|
| Feb 13 |
Introduction and Elimination Rules in HOL (cont) |
slides (full sized PDF)
(six up PDF)
files Demo6.thy
|
|---|
| |
|---|
| Feb 18 |
Quantifier Intro and Elim Rules in HOL |
slides (full sized PDF)
(six up PDF)
files Demo7.thy
|
|---|
| Feb 20 |
Basic Proof Methods |
slides (full sized PDF)
(six up PDF)
files Demo7.thy
|
|---|
| |
|---|
| Feb 25 |
Proof Methods and Intro to Set Theory |
slides (full sized PDF)
(six up PDF)
files Demo8.thy
|
|---|
| Feb 27 |
Inductive Sets |
slides (full sized PDF)
(six up PDF)
files Demo9.thy
|
|---|
| |
|---|
| Mar 4 |
Inductive Relations, General Recursive Functions |
No slides, demo continued from last time
|
|---|
| Mar 6 |
General Recursive Functions, New Type Definitions |
slides (full sized PDF)
(six up PDF)
|
|---|
| |
|---|
| Mar 11 |
Records |
slides (full sized PDF)
(six up PDF)
files Demo11.thy,
|
|---|
| Mar 13 |
Locales |
slides (full sized PDF)
(six up PDF)
files Demo12.thy
|
|---|
| |
|---|
| Mar 18 |
Control Flow Graphs in Isabelle |
files Start of induction example - Scratch.thy
|
|---|
| Mar 20 |
PTRANS |
No slides
|
|---|
| |
|---|
| Mar 25 |
SPRING BREAK |
|
|---|
| Mar 27 |
SPRING BREAK |
|
|---|
| |
|---|
| Apr 1 |
| Blake Petermeier |
Correctness of the Strength Reduction Optimization |
|---|
| Grant Czajkowski |
Correctness of Common Subexpression Elimination |
|---|
| Maria Kotsifakou |
Correctness of Loop Peeling |
|---|
| Kang, Zheng |
Ramsey's Theorem |
|---|
|
|
|---|
| Apr 3 |
| Sean Bartell |
Correctness of a Symbolic Executer for LLVM |
|---|
| Theodoros Kasampalis |
Pointer Analysis for LLVM |
|---|
| Wenjie Zhu |
Dead Code Elimination |
|---|
| me |
The semantics of MiniLLVM |
|---|
|
|
|---|
| |
|---|
| Apr 8 |
| Amarin Phaosawasdi |
Data Dependency in a Subset of C |
|---|
| Taiyu Dong |
Dead Code Insertion |
|---|
| Michael Bay |
Correctness of Skip Insertion |
|---|
| Daejun Park |
Type soundness for IMP |
|---|
|
|
|---|
| Apr 10 |
| Liyi Li |
Something on MSOS |
|---|
| Alex Gyori |
Information Flow |
|---|
| Matt Bauer |
Information Flow |
|---|
| Terence Nip |
Correctness of Redundant Code Elimination |
|---|
|
|
|---|
| |
|---|
| Apr 15 |
| Round 2; |
Preliminary Problem Statement in Isabelle |
|---|
| Amarin Phaosawasdi |
Data Dependency in a Subset of C |
|---|
| Wenjie Zhu |
Dead Code Elimination |
|---|
| Blake Petermeier< |
Correctness of the Strength Reduction Optimization |
|---|
| Grant Czajkowski |
Correctness of Common Subexpression Elimination |
|---|
|
|
|---|
| Apr 17 |
| Kang, Zheng |
Ramsey's Theorem |
|---|
| Theodoros Kasampalis |
Pointer Analysis for LLVM |
|---|
| Sean Bartell |
Correctness of a Symbolic Executer for LLVM |
|---|
| Taiyu Dong |
Dead Code Insertion |
|---|
|
|
|---|
| |
|---|
| Apr 22 |
| Maria Kotsifakou |
Correctness of Code Copying |
|---|
| Michael Bay |
Correctness of Skip Insertion |
|---|
| Daejun Park |
Type soundness fro IMP |
|---|
| |
|
|---|
| Terence Nip |
Correctness of Redundant Code Elimination |
|---|
|
|
|---|
| Apr 24 |
| Liyi Li |
Something on MSOS |
|---|
| Alex Gyori |
Information Flow |
|---|
| Matt Bauer |
Information Flow |
|---|
| |
|
|---|
|
|
|---|
| |
|---|
| Apr 29 |
| Theodoros Kasampalis |
Pointer Analysis for LLVM |
|---|
| Daejun Park |
Type soundness for IMP |
|---|
| Grant Czajkowski |
Correctness of Common Subexpression Elimination |
|---|
| Blake Petermeier |
Correctness of the Strength Reduction
Optimization |
|---|
| Taiyu Dong |
Dead Code Insertion |
|---|
|
|
|---|
| May 1 |
| Kang, Zheng |
Ramsey's Theorem |
|---|
| Maria Kotsifakou |
Correctness of Loop Peeling< Node Copying/td>
|
|---|
| Amarin Phaosawasdi< |
Data Dependency in a Subset of C |
|---|
| Liyi Li |
MSOS |
|---|
| Wenjie Zhu |
Dead Code Elimination |
|---|
|
|
|---|
| |
|---|
| May 6 |
| Sean Bartell |
Correctness of a Symbolic Executer for LLVM |
|---|
| Michael Bay |
Correctness of Skip Insertion |
|---|
| Terence Nip |
Correctness of Redundant Code Elimination |
|---|
| Alex Gyori |
Information Flow |
|---|
| Matt Bauer |
Information Flow |
|---|
|
|
|---|
| |
|---|
