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

precise so that we can use mathematical tools to formalize and check interesting properties
abstract so that properties of interest can be discussed clearly, without getting bogged down in low-level details

Overview: Why study semantics? [2/21]

To prove specific properties of particular programs (i.e., program verification)
- Still fairly labor-intensive
- But important in some domains (safety-critical systems, hardware design, security protocols, inner loops of key algorithms, ...)
To develop intuitions for informal reasoning about programs
To prove general facts about all the programs in a given programming language (e.g., safety or isolation properties)
To deeply understand language features (and their interactions) and develop principles for better language design

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

I'm designing a new web scripting language that's going to take over the world. How can I specify it so that different people implementing compilers will know how it is supposed to behave?
I'm writing a compiler and I'd like to add this optimization, but I'm not convinced it's always correct. How can I be sure?
I want to write a program analysis tool that examines PHP-based websites and checks for possible command injection attacks. How can I know I haven't missed any?

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

A more sophisticated perspective on programs, programming languages, and the activity of programming
- How to view programs and whole languages as formal, mathematical objects
- How to make and prove rigorous claims about them
- Detailed study of a range of basic language features
Powerful mathematical tools for software specification and analysis
- Constructive logic
- Inductive methods of definition and proof
- Hoare logic
- Type systems
Expertise using a cutting-edge mechanical proof assistant

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]

An introduction to programming
A course on functional programming (though we'll be doing some functional programming along the way)
A course on compilers (we will brush on lexical analysis, parsing, abstract syntax, and scope)

Administrivia: Prerequisites [7/21]

CSC447 or my permission.

Administrivia: Course websites [8/21]

Lecture notes: http://fpl.cs.depaul.edu/jriely/535
Lecture recordings: https://col.cdm.depaul.edu/
Discussion: https://piazza.com/depaul/fall2012/csc535/home

Administrivia: Piazza [9/21]

You must sign up for PIAZZA as soon as possible.

https://piazza.com/depaul/fall2012/csc535/home
Free mobile versions for android and ios.

Administrivia: Contact Information [10/21]

Instructor:	James Riely
Home Page:	`http://fpl.cs.depaul.edu/~jriely`
Email:	`[email protected]`
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:

No email
All communication regarding the class should be sent through PIAZZA.
- You can send me personal messages by email.
- You can send course questions by email if you are unable to connect to PIAZZA.
I may send urgent or private messages to you by email.
- Make sure that your email address is correct on CampusConnect.

Contact by phone:

No voicemail
I am happy to talk over the phone any day of the week: you email me your phone # and I will call you back.
My working hours may not be the same as yours, but I will try to be flexible.

Administrivia: Assessment [11/21]

Your grade will be computed from:

Weekly homework: 80% (this includes a take-home final)
Your assignment each week will be to do the exercises rated 2 or higher, including those that are recommended. You can skip the optional exercises.

Each problem will count equally toward your final grade (10 point each).

Hand in homework on COL.
Participation (in class and via PIAZZA): 20%

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

Homework is due before each class.

No late homework.

If you have extenuating circumstances you must tell me at least one week BEFORE the assignment is due.

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.

You must read before class.
You must start homework immediately after class.
You must post questions on PIAZZA two days after homework is assigned, not two days before it is due.

Administrivia: Textbooks [14/21]

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

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

A proof is an indisputable argument for the truth of some mathematical assertion
Proofs are ubiquitous in most branches of computer science
However, unlike proofs in pure mathematics, many CS proofs are very long, shallow, and boring
Can computers help?

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

Different ways of proving theorems with a computer:

Automatic theorem provers find complete proofs on their own
- Huge amount of work, beginning in the AI community in the 50s to 80s
- In limited domains, extremely successful (e.g., hardware model checking)
- In general, though, this approach is just too hard
Proof checkers simply verify proofs that they are given
- These proofs must be presented in an extremely detailed, low-level form
Proof assistants are hybrid tools
- "Hard steps" of proofs (the ones requiring deep insight) are provided by a human
- "Easy parts" are filled in automatically

Coq: Some Proof Assistants [17/21]

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

Isabelle/HOL (Cambridge / Munich)
Twelf (CMU)
Coq (INRIA)
Agda (Chalmers)
...

Coq: The Coq Proof Assistant [18/21]

Developed at the INRIA research lab near Paris over the past 20 years
Based on an extremely expressive logical foundation
- The Calculus of Inductive Constructions
- (hence the name!)
Has been used to check a wide range of significant mathematical results
- Gonthier's fully verified proof of the four-color theorem
- Leroy's verified certifying compiler

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

Rigor
- using Coq forces us to be completely precise about the things we define and the claims we make about them
- Coq's core notions of inductive definition and proof are a good match for the fundamental ways we define and reason about programming languages
Interactivity
- Instant feedback on homework
- Easy to experiment with consequences of changing definitions, different reasoning techniques, etc.
Useful background
- Proof assistants are being used more and more widely in industry and academia
Fun!

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
ProofGeneral in emacs or aquamacs.

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]

There are only a few commands you need to know to use ProofGeneral effectively. They are:
- C-h t: Emacs tutorial.
- C-c C-n: send the next command to Coq.
- C-c C-u: undo (retract) the most recently executed command.
- C-c C-RET: submit everything up to the current cursor location to Coq for processing.
- C-c C-. : move the cursor to the end of the last command which has been processed by Coq.
- C-c . : toggle "electric terminator mode". When this mode is turned on, simply typing a period will send the current command to Coq (normally you have to type a period and then type C-c C-n).
- M-/ : complete the word at the cursor. Hit repeatedly to cycle though options.

I have the following in my emacs initialization file:

;;------------------
;; Proof General
;;------------------
(load-file (expand-file-name "$HOME/Library/packages/ProofGeneral/generic/proof-site.el"))
(eval-after-load "proof-script" '(progn
 ;; these match CoqIDE
 (define-key proof-mode-map [(control meta down)] 'proof-assert-next-command-interactive) ;; C-c C-n
 (define-key proof-mode-map [(control meta up)] 'proof-undo-last-successful-command) ;; C-c C-u
 (define-key proof-mode-map [(control meta right)] 'proof-goto-point) ;; C-c return
 ;; some additional bindings
 (define-key proof-mode-map [(control meta return)] 'proof-goto-point) ;; C-c return
 (define-key proof-mode-map [(control meta .)] 'proof-goto-end-of-locked) ;; C-c C-.
 (define-key proof-mode-map (kbd "C-c C-3") 'proof-three-window-toggle) 
))

Revised: 2007/09/05 06:46