The focus of the seminar this semester will be determined at the start of the semester. Please see previous year links and discussion page for topics currently being considered.
Please note that any future dates may change, and these are only guidelines.
| # |
Day |
Date |
Topic/Reading Due |
Speaker |
Homework Due |
Notes(scribe) |
| 1 |
Mon |
Jan 7 |
Planning and Organization |
Walid Taha |
|
notes(walid) |
| 2 |
Wed |
Jan 9 |
MultithreadedTC |
Nat Ayewah |
|
Slides |
| 3 |
Fri |
Jan 11 |
Discussion |
|
|
|
| 4 |
Mon |
Jan 14 |
|
|
|
|
| 5 |
Wed |
Jan 16 |
Domain Theory (1) |
Corky |
|
notes(Angela) |
| 6 |
Fri |
Jan 18 |
Domain Theory (2) |
Corky |
|
notes(Greg) |
| 6+ |
Mon |
Jan 21 |
No Class (Martin Luther King, Jr.) |
|
|
|
| 7 |
Wed |
Jan 23 |
Domain Theory (3) |
Corky |
|
notes(Jun) |
| 8 |
Fri |
Jan 25 |
Domain Theory (4) |
Corky |
|
notes(Angela) |
| 9 |
Mon |
Jan 28 |
Domain Theory (5) |
Corky |
|
notes(Greg) |
| 9+ |
Mon |
Jan 28 |
Checking types in foreign function calls |
Raj |
|
|
| 10 |
Wed |
Jan 30 |
Abstract |
Karen Wu, Roumen Kaiabachev |
|
Slides, notes(Cherif) |
| 11 |
Fri |
Feb 1 |
Floating-Point Error Analysis Based On Affine Arithmetic & Toward Efficient Static Analysis of Finite-Precision Effects in DSP Applications via Affine Arithmetic Modeling |
Jun |
|
slides notes(Greg) |
| 12 |
Mon |
Feb 4 |
Dependently Typed Pattern Matching. Xi. (summary) (slides) |
Greg |
|
notes(Raj) |
| 13 |
Wed |
Feb 6 |
Physical Modeling for Computer Scientists, Part 1 of 4 |
Alex |
|
slides, notes(Cherif) |
| 14 |
Fri |
Feb 8 |
DML: Eliminating array bound checking through dependent types, Hongwei Xi and Frank Pfenning. PLDI'98. |
Cherif |
|
Slides notes(Greg) |
| 15 |
Mon |
Feb 11 |
A New Representation for Exact Real Numbers (1), Abbas Edalat, Peter John Potts. |
Angela |
|
Slides, notes(Jun) |
| 16 |
Wed |
Feb 13 |
Introduction to Monads |
Walid |
|
notes(Cherif) |
| 17- |
Fri |
Feb 15 |
Physical Modeling for Computer Scientists, Part 2 of 4 |
Alex |
|
slides, notes(Walid&Josh) |
| 17 |
Fri |
Feb 15 |
|
Raj |
|
notes(Angela) |
| 18 |
Mon |
Feb 18 |
A New Representation for Exact Real Numbers (2), Abbas Edalat, Peter John Potts. |
Angela |
|
Slides, notes(Raj) |
| 19 |
Wed |
Feb 20 |
Type Theory and Functional Programming. Simon Thompson (summary) (slides) |
Greg |
|
notes(Cherif) |
| 20 |
Fri |
Feb 22 |
|
Josh |
|
notes(Walid,Cherif) |
| 21 |
Mon |
Feb 25 |
Splint: Statically detecting likely buffer overflow vulnerabilities, D. Larochelle and D. Evans. The 10th USENIX Security Symposium'01. |
Cherif |
|
Slides notes(Greg) |
| 22 |
Wed |
Feb 27 |
A Monadic Approach to Avoiding Code Duplication |
Jun |
|
Slides notes(Angela) |
| 23 |
Fri |
Feb 29 |
Bios for Hifzi Ardi and Roger Post |
SLB visitors |
|
notes(Angela) |
| 23+ |
Fri |
Feb 29 |
|
Josh |
|
|
| 23+ |
Mon |
Mar 3 |
No Class (Midterm Recess) |
|
|
|
| 23+ |
Wed |
Mar 5 |
No Class (Midterm Recess) |
|
|
|
| 23+ |
Fri |
Mar 7 |
No Class (Midterm Recess) |
|
|
|
| 24 |
Mon |
Mar 10 |
|
Raj |
|
|
| 25 |
Wed |
Mar 12 |
LUSTRE: A declarative language for programming synchronous systems. Caspi, Pilaud, Halbwachs, Plaice (summary) (Slides) |
Greg |
|
notes(Angela) |
| 26 |
Fri |
Mar 14 |
End-to-end Security for Web Applications : A Language-based Approach |
Nikhil Swamy |
|
|
| 26+ |
Fri |
Mar 14 |
|
Jun |
|
|
| 27 |
Mon |
Mar 17 |
Formal Verification of Dynamic Properties in an Aerospace Application |
Alex |
|
Slides (Notes) |
| 28 |
Wed |
Mar 19 |
ESPX: Modular checking for buffer over-flows in the large, Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang. ICSE '06. |
Cherif |
|
Slides |
| 29+ |
Fri |
Mar 21 |
An Ideal Model for Polymorphic Recursive Types. David MacQueen?, Gordon Plotkin, Ravi Sethi. (Summary |
Jun |
|
Slides notes (Greg) |
| 29+ |
Fri |
Mar 21 |
Formalizing Real Calculus in Coq Luis Cruz-Filipe. |
Angela |
|
|
| 30 |
Mon |
Mar 24 |
Switched Bond Graphs |
Josh |
|
Slides |
| 31 |
Wed |
Mar 26 |
|
Raj |
|
|
| 32 |
Fri |
Mar 28 |
The PDE2D Collocation Finite Element Method |
Granville Sewell |
|
Slides |
| 32+ |
Fri |
Mar 28 |
|
Jun |
|
|
| 33 |
Mon |
Mar 31 |
A Realizability Model for Impredicative Hoare Type Theory. Morrisett (Summary) (Slides) |
Greg |
|
|
| 34 |
Wed |
Apr 2 |
The First Workshop on Probabilistic and Resilient Architectures for Nanoscale Computing 2008 (PRANACOMP) |
|
|
|
| 34+ |
Fri |
Apr 4 |
No Class (Spring Recess) |
|
|
|
| 35 |
Mon |
Apr 7 |
ESPX: Modular checking for buffer over-flows in the large, Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang. ICSE '06. |
Cherif |
|
Slides |
| 36 |
Wed |
Apr 9 |
Introduction to physical modeling with modelica, Michael M. Tiller. |
Angela |
|
|
| 37 |
Fri |
Apr 11 |
Matlab D: Compiling Parallel Matlab with User-Defined Data Distributions (Duncan Hall 3076) |
Mary Fletcher |
|
|
| 38 |
Mon |
Apr 14 |
Discussion for next semester |
|
|
notes(Angela) |
| 39 |
Wed |
Apr 16 |
Intro to Dynamic System Stability |
Josh |
|
Slides (Notes) |
| 40 |
Fri |
Apr 18 |
Hoare Type Theory & Separation Logic. (Slides) |
Gregory |
|
|
| 41 |
Mon |
Apr 21 |
Acumen modeling of an open hole tractor with tracks (Spare lecture 4) |
Alex |
|
slides |
| 42 |
Wed |
Apr 23 |
Fault Tolerance (9:00 am) |
Robert Hanmer |
|
notes(Walid,Cherif) |
| 42+ |
Wed |
Apr 23 |
Planning for next semester |
Walid |
|
|
| 43 |
Mon |
Apr 28 |
Heifer: A Type Theory for Creating Programming Languages |
Edwin Westbrook |
|
|
| 44 |
Thu |
May 8 |
Computing While Compiling: Reasons and Methods for Compile-time Metaprogramming |
Ronald Garcia |
|
|
Students with disabilities are encouraged to contact me during the first two weeks of class regarding any special needs. Students with disabilities should also contact Disabled Student Services in the Ley Student Center and the Rice Disability Support Services.
Teaching Web 
Create New Topic 
Index 
Search 
Changes 
Notifications 
Statistics 
Preferences
Log In
This work is licensed under a Creative Commons Attribution 2.5 License. Please follow our citation guidelines.