CSC535: Semantics of Programming Languages (Fall AY12/13)
James Riely

News

2012/09/03 16:50

Welcome to the course home page! Lecture slides are to the right, and useful links are to the left.

Important Links

Software Foundations

Software Foundations (local)

Certified Programming with Dependent Types

Lecture Materials

1.		Numbers, lists, basic proofs [09/05]
		Administrative Information Preface: (html) Basics: (html) (coq) (homework) Lists: (html) (coq) (homework)

2.		Polymorphism, functions as data [09/12]
		Poly: (coq) (html) (homework)

3.		Propositions and evidence [09/19]
		Gen: (coq) (html) Prop: (coq) (html) (homework)

4.		Logic in Coq [09/26]
		Logic: (coq) (html) (homework)

5.		Imperative programs [10/03]
		Imp: (coq) (html) (homework) SfLib: (coq) ImpParser: (coq) (html) ImpCEvalFun: (coq) (html)

6.		Program equivalence [10/10]
		Equiv: (coq) (html) (homework)

7.		Hoare logic [10/17]
		Hoare: (coq) (html) (homework) HoareList: (coq) (html) HoareAsLogic: (coq) (html)

8.		Small step semantics [10/24]
		Rel: (coq) (html) Smallstep: (coq) (html) (homework)

9.		Types [10/31]
		Types: (coq) (html) (homework)

10.		Simply typed lambda calculus [11/07]
		Stlc: (coq) (html) (homework)

11.

Take-home final due [11/14]

Contact Hours

Class Hours:	Wed 5:45pm-9:00pm in CDM 222 [Section 701]
	Online, Anytime [Section 710]
Office Hours:	Wed 1:00-2:00pm in CDM 846

The stylesheets used to create this website are based on Corin Pitcher's XSLT stylesheets for lecture slides.