| Schedule subject to change as course progresses. |
|---|
| Lecture slides for not yet given lectures are preliminary, and may change. |
|---|
| Jan 17 |
Course Introduction & Introduction to Operational Semantics |
slides (full sized PDF)
(six up PDF)
files Demo1.thy
|
|---|
| Jan 19 |
Intro continued |
slides (full sized PDF)
(six up PDF)
files Demo2.thy, assume style
files Demo2.thy, isar style
|
|---|
| |
|---|
| Jan 24 |
Basic Isabelle syntax |
slides (revised) (full sized PDF)
(six up PDF)
|
|---|
| Jan 26 |
Introducing new types and terms |
files Demo3.thy
|
|---|
| |
|---|
| Jan 31 |
Rewriting Simplification |
slides (full sized PDF)
(six up PDF)
files Demo4.thy
|
|---|
| Feb 2 |
Basic Introduction and Elimination Rules in HOL |
slides (full sized PDF)
(six up PDF)
files Demo5.thy
|
|---|
| |
|---|
| Feb 7 |
Introduction and Elimination Rules in HOL (cont) |
slides (full sized PDF)
(six up PDF)
files Demo6.thy
|
|---|
| Feb 9 |
Introduction and Elimination Rules in HOL (cont) |
slides (full sized PDF)
(six up PDF)
|
|---|
| |
|---|
| Feb 14 |
Quantifier Intro and Elim Rules in HOL |
slides (full sized PDF)
(six up PDF)
files Demo7.thy
|
|---|
| Feb 16 |
|
slides Contiuned from last time
|
|---|
| |
|---|
| Feb 21 |
Proof Methods and Intro to Set Theory |
slides (full sized PDF)
(six up PDF)
files Demo8.thy
|
|---|
| Feb 23 |
Inductive Sets |
slides (full sized PDF)
(six up PDF)
files Demo9.thy
|
|---|
| |
|---|
| Feb 28 |
Inductive Relations, General Recursive Functions |
slides (full sized PDF)
(six up PDF)
|
|---|
| Mar 1 |
General Recursive Functions, New Type Definitions |
slides (full sized PDF)
(six up PDF)
|
|---|
| |
|---|
| Mar 6 |
Isar Overview |
slides (full sized PDF)
(six up PDF)
files IsarDemo1.thy,
IsarDemo2.thy
|
|---|
| Mar 8 |
New Types, Records |
Slides continued from lecture 14
files Demo10.thy
|
|---|
| |
|---|
| Mar 13 |
Records |
files Demo11.thy
|
|---|
| Mar 15 |
Locales |
files Demo12.thy
|
|---|
| |
|---|
| Mar 20 |
SPRING BREAK |
|
|---|
| Mar 22 |
SPRING BREAK |
|
|---|
| |
|---|
| Mar 27 |
Example presentation of a project |
|
|---|
| Mar 29 |
|
|
|---|
| |
|---|
| Apr 3 |
| Liyi Li |
Syntax and Semantics of CSPP |
|---|
| Ryan Hitchman |
Proof of correctness of A* |
|---|
| Kyle Blocher |
Syntax and Semantics of IMP |
|---|
|
|
|---|
| Apr 5 |
| David Lazar |
Properties of functions in Haskell Prelude |
|---|
| Xioakang Qiu |
Separation Logic |
|---|
| Susannah Johnson |
Translation of EOFMC in Concurent Game Structures |
|---|
|
|
|---|
| |
|---|
| Apr 10 |
| Dale Frampton |
Dijkstra's Algoritm |
|---|
| Choonghwan Lee |
Slicing |
|---|
| Chad DeLoatch |
microJava |
|---|
|
|
|---|
| Apr 12 |
| Pranav |
Separation Logic |
|---|
| Round 2 |
|---|
| Liyi Li |
Syntax and Semantics of CSPP |
|---|
| Kyle Blocher |
Syntax and Semantics of IMP |
|---|
|
|
|---|
| |
|---|
| Apr 17 |
| Ryan Hitchman |
Proof of correctness of A* |
|---|
| Xioakang Qiu |
Separation Logic |
|---|
| David Lazar |
Properties of functions in Haskell Prelude |
|---|
|
|
|---|
| Apr 19 |
| Susannah Johnson |
Translation of EOFMC in Concurent Game Structures |
|---|
| Choonghwan Lee |
Slicing |
|---|
| Pranav |
Separation Logic |
|---|
|
|
|---|
| |
|---|
| Apr 24 |
| Dale Frampton |
Dijkstra's Algoritm |
|---|
| Chad DeLoatch |
microJava |
|---|
| Round 3 |
| Liyi Li |
Syntax and Semantics of CSPP |
|---|
| Kyle Blocher |
Syntax and Semantics of IMP |
|---|
|
|
|---|
| Apr 26 |
| Ryan Hitchman |
Proof of correctness of A* |
|---|
| David Lazar |
Properties of functions in Haskell Prelude |
|---|
| Xioakang Qiu |
Separation Logic |
|---|
| Susannah Johnson |
Translation of EOFMC in Concurent Game Structures |
|---|
|
|
|---|
| |
|---|
| May 1 |
| Choonghwan Lee |
Slicing |
|---|
| Pranav |
Separation Logic |
|---|
| Chad DeLoatch |
microJava |
|---|
| Dale Frampton |
Dijkstra's Algoritm |
|---|
|
|
|---|
| |
|---|
