...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Course Introduction
Dr. Mattox Beckman
Illinois Institute of Technology
Department of Computer Science
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Objectives
Learn who your instructor is;
Understand how this course will be administered, including
your responsibilities as a student, and
the instructors responsibilities to you.
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
The Instructor
Name Mattox Beckman
Education PhD, Fall 2003, University of Illinois at
Urbana-Champaign
Research Interests Programming Languages, Type Theory, Functional
Programming
Professional Interests Teaching, Category Theory, Consulting, Clojure
Personal Interests Fermentation (Beer, Wine, Sauerkraut), Go (Baduk,
Wei-Qi, Igo), Christian Theology, Insight Meditation,
Attic/Koine Greek, Korean, Carbohydrate Restriction
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
My Responsibilities
My job is to provide an optimal learning environment.
Assignments will be clearly written and administered.
Questions will be answered in a timely fashion.
Objectives of lectures and assignments will be clearly
communicated.
Grades will be fair, meaningful, and reect mastery of course
material.
C grade means can reliably recognize the correct answer
A grade means can reliably generate the correct answer
If somethings not going the way it should, tell me!
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Your Responsibilities
Check the course web page frequently.
[Link]
Subscribe to Piazza and have at least digest email.
Do the homework assignments in order to learn them.
Attend lectures if at all possible.
Take responsibility and initiative in learning material experiment!
You are the one primarily responsible for your education.
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Contact Info
Instructor Mattox Beckman
Best Contact via email. I use inbox zero, but not on
weekends.
Email Addresses <beckman@[Link]>
Ofce 110 SB
Ofce Hours Tuesday and Thursday, 16.0017.00;
and by appointment.
Home Page [Link]
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Activities
Collectively worth 20%
Designed to help you study for the exams, and to achieve major
course objectives.
Full collaboration allowed.
Expect at least one each class period.
These are due the following class, no late activities accepted.
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Exams
The purpose of an exam is to measure mastery of material.
1 midterm exam worth 40%.
Date: June 26
Location: in class.
Final exam worth 40%.
Thursday, July 24, in class.
It will be cumulative. Nice British System
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Grade Guarantees
The course will not be graded on a curve or by ranking. Instead, we have
the following grade guarantees:
85% A
70% B
55% C
40% D
Note that a graduate student cannot be assigned a D grade. Below 55%
is failing!
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Workow
Here is the typical workow for a lecture period.
Visit the Schedule Page the day before the lecture.
Watch the online video.
Come to class
First 15 minutes, Q and A
Remaining time: in-class assignment (activity)
Activities due by the end of the next class. (Hard Deadline!)
Online students: submit by email.
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Attention vs. Time
Why activities?
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Levels of Learning Retention
1. Hearing it in lecture you will forget most of it.
2. Writing it down improved learning retention.
3. Solving a problem
4. Explaining a concept This requires a team activity
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
In-class activities
Research shows that students learn a lot more in active learning
environments. So...
Bring a pen or iPad!
Most activities will be team-based.
Answers will typically not be handed out, but they will be discussed
in class and may be online.
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
What is this course about?
Two word answer: Program Verication
Outline of the Course
Introduce Formal Systems
Review First Order Predicate Logic
Introduce a small imperative language
Design a Proof System for it
And then start adding features....
...
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
...
.
.
.
..
.
.
.
..
.
.
.
. . . . .
Objectives
. . .
Grades
. . . .
Lectures
. .
Content
Features
Our technique is simple.
Add a new language feature.
Disjoint Parallelism
Shared Variables
Atomic Regions
Nondeterminism
Messages
Show how to translate this feature into a previously proved
language.
