CS 6115 (Spring 2015)

Certified Software Systems
TR 8:40-9:55
Hollister 406

Projects

Schedule

A list of potential papers is here.
Date Topic Notes Reading Presenter
22 JanuaryNo class (Foster away)
27 JanuaryIntroductionBasics.v
29 JanuaryInductionInduction.v
3 FebruaryDatatypes and PolymorphismLists.v Poly.v
5 FebruaryTacticsMoreCoq.v
9 FebruaryNo class (Foster away)
11 FebruaryNo class (Foster away)
17 FebruaryNo class (February Break)
19 FebruaryLogicLogic.v Prop.v MoreLogic.v
24 FebruaryIMPImp.v ImpCEvalFun.v
26 FebruaryOptimizationEquiv.v PE.v
3 MarchNo class (Foster away)
5 MarchAutomationHoare.v Hoare2.v SmallStep.v Auto.v
10 MarchVerified Compilers[DLP] [H]Foster
12 MarchCompCert[L]Foster
17 MarchCalculus of Constructions[CH]Long
19 MarchRockSalt[MTTTG]Nkounkou
24 MarchNo class (Foster away)
26 MarchNo class (Foster away)
31 MarchNo class (Spring Break)
2 AprilNo class (Spring Break)
7 AprilNo class (Foster away)
9 AprilMechanized Metatheory[ACCPW]Smolka
14 AprilWeb Programming[C]Leung
16 AprilCompositional CompCert[SBCA]Loring
21 AprilVellvm[ZNMZ]Foster
23 AprilNo class (Foster away)
28 AprilVerified Browser Shims[JTL]Wang
30 AprilOS Verification[YH]Muehlboeck
8 MayFinal Project Presentations
Validate XHTML Validate CSS
Last updated January 2015