Course personnel | Textbooks | Readings | Schedule | Coq Proof Assistant | Links

Course personnel

Instructor Phone Email Course Time Place
Yu Zhang 3603804 yuzhang at ustc.edu.cn Thursday 13:30~15:55P.M. 3321

Textbooks

Supplementary Readings

  1. C.A.R. Hoare. Hints on programming language design. Stanford University. Technical Report: CS-TR-73-403. 1973. .pdf
  2. Niklaus Wirth(Pascal之父). On the Design of Programming Languages. Information Processing. 74, pages 386-393, New York, N.Y., 1974. North-Holland Publishing Co. .pdf
  3. Peter Wegner. Programming languages - the first 25 years. IEEE Transactions on Computers, Vol. C-25, No. 12, pp. 1207-1225, 1976. .pdf
  4. Guy L. Steele. Growing a Language. OOPSLA 1998 Keynote. .pdf
  5. C.A.R. Hoare. An axiomatic basis for computer programming. CACM 12(10), 1969, pages 576 - 580. .pdf
  6. Leslie Lamport. The Future of Computing: Logic or Biology. .pdf
  7. Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing. June 2000, updated November 2000. .pdf
  8. ......

Coq Proof Assistant

Schedule

Date Topics Homework Readings/Coq Practice
Sep.11
Sep.18		 1 Intro(.pdf1in1, 6in1)
[TPL]ch1;[TAPL]ch1~3;		 Sep.11:1.1; Sep.18:1.2,1.3
Due:Sep.25
  • Read Supplementary Readings and write a reading report.(Due: before Oct.8 23:00)
  • Oct.9 Please read the reports.rar, and give the sort order (i.e.,1, 2, 3 ,...; the best is sorted as 1) of all reports. (Due: before Oct.15 23:00)
    • Sep.18
    Sep.25         		2 Judgement and Rules(.pdf1in1, 6in1)
  • Inductive definitions
  • Hypothetical judgements
  • Parametric judgements
    [PFPL]ch1~3
    		• [PFPL 1.9]1,2
    Due:before Oct.22 23:00(in Coq,
    submitted by email)>

    Sep.25 Coq Introduction 1(.pdf1in1, 6in1)

  • Declarations and Definitions: bnat_1.v
  • Proposition logical verification: prop.v
    Tactics: intro(s), split, left, right, exact, apply
  • Submit your answer on prop.v & bnat_1.v by email before Oct.15 23:00.
    • Sep.25
    Oct.9
    Oct.16
    Oct.23
    Oct.30     		3 A simple Language L{num,str}(.pdf1in1, 6in1)
  • Syntactic Objects
  • Concrete syntax
  • Abstract syntax
  • Static Semantics
  • Dynamic Semantics
  • Type Safety
    [PFPL]ch5~13
    		• [PFPL 6.2]2
    Due:before Oct.22 23:00
    [PFPL 11.4]1, 2
    		 Oct.16 Coq Introduction 2(.pdf1in1, 6in1)

  • Symbols and strings: sym_str1.v, util.v
  • Tactics: intros, simpl, assumption, apply, reflexivity, rewrite, constructor, induction, destruct, unfold

    Oct.23 Coq Practices
  • propsol.v,bnat_1sol.v,sym_str1sol.v, pfpl_1_9.v
  • forall, exists; fixpoint vs. proposition
  • Tactics: decompose, transitivity, inversion, destruct, elim, trivial, subst, auto, a series of tactics separated by commas
  • Please practice on pfpl_1_9.v, try to implement [PFPL 6.2]2 in coq(Due:before Nov.5 23:00), learn the built-in types in coq yourselves, such as list, etc.
    • Oct.30
    Nov.6
    Nov.13     		4 Simple Types(.pdf1in1, 6in1)
  • Functions
  • Products
  • Sums
  • Recursive Function
  • Recursive Type
    [PFPL]ch14, 17, 18, 15, 16
    		• [slides]4.1 Nov.6 Coq Practices: B.C. Pierce's lecture
  • lec01.v: Pair, List
  • lec02.v: Option, High-order function, Polymorphism, Currying and uncurrying
    Nov.13 Coq Practices: pfpl_1_9sol.v
    • Nov.20
    Nov.27
    Dec.4     		5 Dynamic Typing(.pdf1in1, 6in1)
  • Untyped lambda calculus
  • Dynamic typing
    [PFPL]ch22,23
    		• [slides]5.1~5.2, 5.3~5.4
    Dec.4
  • 6 Propositions and Types(.pdf1in1, 6in1)
  • Curry-Howard Imorphism
  • Constructive logic & classical logic
    [PFPL]ch32,33
    • Dec.4
    Dec.11
    Dec.18     		7 Control Flow(.pdf1in1, 6in1)
  • Abstract Machine for Control
  • Exceptions
  • Continuations
    [PFPL]ch29~31
    		• Dec.11 Coq Practices: Understand the formalization of L{num, str} in coq, try to formalize other languages in coq.
    A good link for learning coq
    Dec.18 Last year's lectures:
    Storage effect
    Polymorphism
    Subtyping     		Notice: Everyone must submit his report before Jan. 14 22:00.

    Links

    visitors since 09/13/2008.