CSC535: Lecture 1 (Numbers, lists, basic proofs)

Contents [0/21]

Overview: What is semantics? [1/21]
Overview: Why study semantics? [2/21]
Overview: Questions This Course Could Help Answer [3/21]
Overview: What you'll get out of the course [4/21]
Overview: Syllabus [5/21]
Overview: What this course is not [6/21]
Administrivia: Prerequisites [7/21]
Administrivia: Course websites [8/21]
Administrivia: Piazza [9/21]
Administrivia: Contact Information [10/21]
Administrivia: Assessment [11/21]
Administrivia: Attendance [12/21]
Administrivia: Expectations [13/21]
Administrivia: Textbooks [14/21]
Coq: What is a Proof? [15/21]
Coq: What is a Proof Assistant? [16/21]
Coq: Some Proof Assistants [17/21]
Coq: The Coq Proof Assistant [18/21]
Coq: Why Use Coq in This Course [19/21]
Coq: How to get Coq [20/21]
Coq: Using ProofGeneral [21/21]

Overview: What is semantics? [1/21]

Semantics is the mathematical study of the meaning of programs.

The goal is finding ways to describe program behaviors that are both precise and abstract.

Overview: Why study semantics? [2/21]

Overview: Questions This Course Could Help Answer [3/21]

Overview: What you'll get out of the course [4/21]

Overview: Syllabus [5/21]

1. Foundations 
   1.1 Functional programming 
   1.2 Inductive definitions and proof techniques 
   1.3 Constructive logic 
   1.4 The Coq proof assistant 

2. Reasoning about programs
   2.1 Specifying a simple imperative language
   2.2 Operational semantics
   2.3 Hoare Logic
   2.4 Information-flow security (*)

3. Type systems
   3.1 Simply typed lambda-calculus
   3.2 Type safety
   3.3 Subtyping (*)

(*) If time permits

Overview: What this course is not [6/21]

Administrivia: Prerequisites [7/21]

CSC447 or my permission.

Administrivia: Course websites [8/21]

Administrivia: Piazza [9/21]

You must sign up for PIAZZA as soon as possible.

Administrivia: Contact Information [10/21]

Instructor:James Riely
Home Page:http://fpl.cs.depaul.edu/~jriely
Email:jriely@cs.depaul.edu
Phone:1.312.362.5251
Address: School of Computing, DePaul University
243 South Wabash Avenue
Chicago, IL 60604-2301
Office:CDM 846
Office Hours: Wed 1:00-2:00pm in CDM 846
Class Page:http://fpl.cs.depaul.edu/jriely/535
Class Hours: Wed 5:45pm-9:00pm in CDM 222 [Section 701]
Online, Anytime [Section 710]

Contact by email:

Contact by phone:

Administrivia: Assessment [11/21]

Your grade will be computed from:

You are encouraged to collaborate on homework assignments in small groups (two is ideal).

Homework is due before each class.

No late homework.

No extra credit.

DePaul's academic integrity policy

Administrivia: Attendance [12/21]

In-class students must attend class.

Online students must watch the class within 24 hours.

Administrivia: Expectations [13/21]

The course requires you to actively engage the material.

Administrivia: Textbooks [14/21]

We are using an online book available from the course homepage.

Coq: What is a Proof? [15/21]

Coq: What is a Proof Assistant? [16/21]

Different ways of proving theorems with a computer:

Coq: Some Proof Assistants [17/21]

There are now a number of mature, sophisticated, and widely used proof assistants...

Coq: The Coq Proof Assistant [18/21]

Coq: Why Use Coq in This Course [19/21]

Coq: How to get Coq [20/21]

We will use coq 8.3

8.4 will not work.

  Windows/mac: easy.
  UbuntuLinux: sudo apt-get install coqide

For editing, you can use

Coqide is easy to install and use, but its keybindings stink on the mac (it does not understand the command key).

You can change the keybindings (undo, in particular) by following these instructions: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release the mouse button afterwards.

Coq: Using ProofGeneral [21/21]


Revised: 2007/09/05 06:46