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 |
|
|
|