Programming Language Foundations 2023/24 fall

Lectures & Homework

We will go through a number of chapters in LF and PLF. For homework, you need to submit the same chapter files. Some chapters introduce new tactics or syntax but most are about practicing theorem proving in some new aspect. See the goals for each chapter.

Lectures

Lecture	Chapter	Notes
(1) 7. sept	Basics.v
(2) 8. sept	Basics.v Induction.v	Basics.v due on Sept 15th
(3) 14. sept	Induction.v Lists.v	Induction.v due on Sept 21st
(4) 15. sept (video only)	Lists.v Poly.v	Lists.v and Poly.v due on Sept 22nd
(5) 21. sept	Tactics.v
(6) 22. sept (video only)	Tactics.v Logic.v
(7) 28. sept	Logic.v	Video from 2022, Tactics.v due on Oct 5th
(8) 29. sept (video only)	Logic.v	Video from 2022, Logic.v due on Oct 6th
(9) 5. okt	IndProp.v
(10) 6. okt (video only)	IndProp.v
(11) 12. okt	IndProp.v Maps.v	IndProp.v due on Oct 19th
(12) 13. okt (video only)	Maps.v
(13) 19. oct	Imp.v	Maps.v due on Oct 26th
(14) 20. oct (video only)	Imp.v Auto.v	Imp.v and Auto.v due on Oct 27th
(15) 26. oct	ProofObjects.v
(16) 27. oct (video only)	ProofObjects.v	Auto.v due on Nov 2nd
() 2. nov	(no lecture)
(17) 3. nov (video only)	Equiv.v
(18) 9. nov	Equiv.v Hoare.v
(19) 10. nov (video only)	Hoare.v
(20) 16. nov	Hoare.v
(21) 17. nov (video only)	Hoare.v	Equiv.v and Hoare.v due on Nov 23rd
(22) 23. nov	Hoare2.v
(23) 24. nov (video only)	Hoare2.v	Hoare2.v due on Dec 1st
(24) 30. nov (video only)	HoareAsLogic.v	HoareAsLogic.v due on exam date
() 1. dec (video only)	(no lecture)
(25) 7. dec	Smallstep.v
(26) 8. dec (video only)	Smallstep.v
(27) 14. dec	Smallstep.v Types.v	Hoare2.v due on exam date
(28) 15. dec (video only)	Types.v	Type.v due on exam date
(28) 20. dec	(No more lecures)	Personal consultation if necessary

LF

Preface.v

• Goal: talk about the course

Basics.v

• Goal: base FP language, proof language, simple proofs

1. Data and Functions
   • tactics: simpl, reflexivity
2. Proof by Simplification, Proof by Rewriting
   • tactics: intros
3. Proof by Case Analysis
   • bullets
   • tactics: destruct X as eqn:Y

Induction.v

• Goal: induction on natural numberss

1. Separate compilation
2. Proof by Induction
   • tactics: induction
3. Proofs Within Proofs
   • tactics: assert
4. Formal vs. Informal Proof
5. More exercises
   • tactics: replace

Lists.v

• Goal: look at data structures

1. Pairs of Numbers
2. Lists of Numbers
3. Bags via Lists
4. Reasoning About Lists, Induction on Lists, List Exercises
5. Options
6. Partial Maps

Poly.v

• Goal: look at almost std. lib. definitions, exercises

1. Polymorphic Lists
2. Polymorphic Pairs
3. Polymorphic Options, Functions as Data, Anonymous Functions
4. Map
5. Fold
6. Functions That Construct Functions

Tactics.v

1. Goal: provide tools to theoretically prove almost anything
2. The [apply] Tactic
   • tactics: apply
   • exercises: silly_ex, apply_exercise1
3. The [apply with] Tactic
   • tactics: apply with
4. The [injection] and [discriminate] Tactics
   • tactics: injection, discriminate
5. Using Tactics on Hypotheses
   • tactics: apply in
6. Varying the Induction Hypothesis
   • tactics: generalize dependent
7. Unfolding Definitions, Using [destruct] on Compound Expressions
   • tactics: unfold
8. Additional Exercises

Logic.v

• Goal: more tools for easier proving of logic idioms

1. the Prop type, Logical Connectives
2. Falsehood and Negation
3. Truth, Logical Equivalence
4. Setoids and Logical Equivalence
5. Existential Quantification
6. Programming with Propositions
7. Applying Theorems to Arguments
8. Functional Extensionality
9. Propositions vs. Booleans, Working with Decidable Properties
10. Classical vs. Constructive Logic

IndProp.v

• Goal: Safely adding theories/assumptions

1. The Collatz Conjecture, Transitive Closure, Permutations, Evenness
2. Using Evidence in Proofs
3. Induction on Evidence
4. Inductive Relations
5. A Digression on Notation
6. Case Study: Regular Expressions
   • tactics: remember
   • weak_pumping (hint: finish 1st App case and copy-paste the rest, lemmas: app_length, add_le_cases, rewrite app_assoc, plus_le, pumping_constant_0_false hint: destruct s1 in MStarApp case)
7. Case Study: Improving Reflection

Maps.v

• Goal: more data structures and exercises

1. The Coq Standard Library, Identifiers, Total Maps
2. Partial Maps

Imp.v

• Goal: exercise tactic(al)s and inductives

1. Arithmetic and Boolean Expressions, Coq Automation
   • tactics: ;, try, repeat, lia, clear, rename, assumption, contradiction, constructor
2. Evaluation as a Relation
3. Expressions With Variables, Commands, Evaluating Commands
4. Additional Exercises

Auto.v

• Goal: automatically proving (large number) of simple cases

ProofObjects.v

• Goal: Proofs are programs and programs are proofs

1. Proof Scripts
2. Quantifiers, Implications, Functions
3. Programming with Tactics
4. Logical Connectives as Inductive Types
5. Equality
6. Coq's Trusted Computing Base
7. More Exercises
8. Proof Irrelevance (Advanced)

PLF

Equiv.v

• Goal: exercise proofs of stateful programs

1. Behavioral Equivalence
2. Properties of Behavioral Equivalence
3. Program Transformations
4. Proving Inequivalence

Hoare.v

• Goal: Standard way of proving properties of imperative programs

1. Assertions
2. Hoare Triples
3. Proof rules
4. Summary
5. Additional exercises

Hoare2.v

• Goal: Standard way of proving properties of imperative programs

1. Decorated Programs
2. Formal Decorated Programs
3. Finding loop invariants

HoareAsLogic.v

• Goal: Theoretical side of Hoare triples

1. Hoare Logic and Model Theory
2. Hoare Logic and Proof Theory
3. Derivability
4. Soundness and Completeness
5. Postscript: Decidability

Smallstep.v

• Goal: Shows how to give meanings to programs

1. A Toy Language
2. Relations
3. Multi-Step Reduction
4. Small-Step Imp
5. Concurrent Imp
6. A Small-Step Stack Machine
7. Aside: A normalize Tactic

Types.v

• Goal: Types that will give guarantees later

1. Typed Arithmetic Expressions

Stlc.v

• Goal: Define simply typed lambda-calculus

1. Overview
2. Syntax
3. Operational Semantics
4. Typing

StlcProp.v

• Goal: Now having types gives us guarantees

1. Canonical Forms
2. Progress
3. Preservation
4. Type Soundness
5. Uniqueness of Types
6. Context Invariance (Optional)