COMP 617S07: Seminar in Resource Aware Programming (Spring 2007)

Instructor:	Walid Taha	Lectures:	Duncan Hall (DH) 3110	Time:	MWF 11:00-12:00 pm

Here is a link to last semesters seminar.

Related Seminars: COMP 635 Heterogeneous Processors

---

Introduction

This focus of this semester will be on understanding what programming style is possible with Concoqtion, and especially in applications such as staged interpreters and circuit design. We will consult sources such as TAPL, ATTPL and the CoqArt book.

During the course, we will use Concoqtion to implement various interesting algorithms, and document what we learn. We will study the basic meta-theoretic properties that arise in the design of Concoqtion.

Plan: To gain experience programming in Concoqtion, we will work on systematically implementing the following functions in Concoqiton, and reporting our experience on implementing them (as comments in the code). In each of the cases, we should focus initially on functional versions, and then see if the ideas can carry over to the imperative setting. Please check and update known bugs in Concoqtion regularly.

Problem	References	Angela	Cherif	Dan	Joseph	Jun	Summary
Lists		X	X	X	X	X	X
Braun_trees	red-black trees, Braun trees, Three Algorithms on Braun Trees	X	X	X	X	X	X

• lists (map, zip, size_it, at_size)
• balanced trees
• sorting on lists (merge sort, insert sort, quick sort)
• circuits
  • adder: n bit -> n bit -> n+1 bit
  • encoder: n bit -> 2^n bit
  • decodr: 2^n bit -> n bit
• tries
• matrix operations
• well-typed terms, type preserving substitution
• type-preserving program transformations
• simple interpreters
• parsers
• printf
• various abstractions: objects, variant types, classes, modules
• syntax with free variables, variable-aware types for substitution
• safe threading
• low-level code: typed assembly language (including VM's), Cyclone-in-OCaml, device drivers, systems code, network code, etc
• phantom types for capabilities
• resource-bound certification

Recommended Background Text: Types and Programming Languages, Benjamin Pierce.

Recommended Reading:

• Mark Jones, First class polymorphism with nested types
• Karl Crary and Stephani Weirich, resource bound certification
• Christine Paulin-Mohring, course on inductive definitions

Course Schedule

Please note that any future dates may change, and these are only guidelines.

#	Day	Date	Reading Due	Speaker	Homework Due	Notes
1	Mon	Jan 8		Walid Taha
2	Wed	Jan 10	TPL Ch 1	Walid Taha	download and install Concoqtion. Read the Concoqtion user manual. Write and compile the definition of sized lists, as well as some simple functions on sized lists	Sized lists in Concoqtion
3	Fri	Jan 12	Start ATTPL Ch 2	Walid Taha	Use Concoqtion to write the list map function on sized lists. Be prepared to explain and discuss your implementation in class	Hindley-Milner vs. Concoqtion
3+	Mon	Jan 15	Marting Luther King, Jr. day (no class)
4	Wed	Jan 17	Complete ATTPL Ch 2	Class Cancelled (Catastrophic Weather)	Start thinking about defining a type for balanced binary trees in Concoqtion
5	Fri	Jan 19	PEPM 2007 Concoqtion paper	Emir Pasalic	Complete implementation of balanced binary trees in Concoqtion
6	Mon	Jan 22	typeful programming paper	Emir Pasalic	In class, we will start discussing how each of these concepts can be implemented in Concoqtion
7	Wed	Jan 24	Coq (continued)	Emir Pasalic	Some in-class notes	Programming in Coq and Comparisons to Concoqtion
8	Fri	Jan 26	Coq (continued)	Emir Pasalic
9	Mon	Jan 29	Existentials	Walid Taha		Writing Existentials in Concoqtion and Other Tricks to Implement Functions on Sized Lists
10	Wed	Jan 31	Sized lists functions	Walid Taha	Additional Functions that Operate on Sized Lists
11	Fri	Feb 2		Walid Taha		Type and Implementation of Function "at_size"
12	Mon	Feb 5		Walid Taha		Benchmarks, interaction of indexed types with other things, OCaml match
13	Wed	Feb 7		Walid Taha		Performance Measurement & First view on balenced trees
14	Fri	Feb 9		Walid Taha		Fold Function
15	Mon	Feb 12		Walid Taha		Notes for Feb 12
16	Wed	Feb 14		Walid Taha		Notes for Feb 14
17	Fri	Feb 16		Eric Allen	Guest Talk	Fortress and Object-Oriented Programming
18	Mon	Feb 19		Walid Taha		structural induction; induction by halving instead of decrementing
19	Wed	Feb 21		Walid Taha		Context Refinement
20	Fri	Feb 23		Walid Taha		Notes for Feb 23
21	Mon	Feb 26		Walid Taha		Staged Interpreters(1)
22	Wed	Feb 28				Staged Interpreters(2)
23	Fri	Mar 2		Angela Zhu:	Reference	Staged Interpreters(3)
23+	Mon	Mar 5	spring break (no class)
23+	Wed	Mar 7	spring break (no class)
23+	Fri	Mar 9	spring break (no class)
24	Mon	Mar 12				Polymorphic Recursion
25	Wed	Mar 14				Category Theory
26	Fri	Mar 16				The "as" effect on context refinement, Type checker
27	Mon	Mar 19				Cast; Inhabitance
28	Wed	Mar 21				Notes for March 21
29	Fri	Mar 23		Emir	Multi-stage Programming: Its Theory and Applications
29+	Fri	Mar 23		Joseph Young	Typing Sparse Matrices
30	Mon	Mar 26		Dan&Jun		Sorting Algorithms (1)
31	Wed	Mar 28		Joseph Young	How to Extract OCaml Types in Coq and Use them in a Certified Interpreter	Extracting OCaml types in Coq
32	Fri	Mar 30		Angela&Cherif		Dependent Types in the FFT
33	Mon	Apr 2		Angela&Cherif		Dependent Types in the FFT (cont...)
34	Wed	Apr 4		Emir		Staging
34+	Fri	Apr 6	spring recess (no class)
35	Mon	Apr 9		Dan&Jun		Sorting Algorithms (2)
36	Wed	Apr 11		Emir		How a Type System Can be Used as a Proof System
37	Fri	Apr 13		Walid Taha		Curry-Howard Isomorphism, FFT project discussion
38	Mon	Apr 16		Joseph Young	Writing a Certified Interpreter in OCaml Using Coq	Programming in Coq Using Extraction
39	Wed	Apr 18		Walid Taha		Product (Big Pi) Types
40	Fri	Apr 20		Walid Taha		Done and TODOs
41	Mon	Apr 23		Walid Taha		Multi-staging
42	Wed	Apr 25		Walid Taha

Accomodations for Students with Special Needs

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.

Access Control: (Please don't edit)

• Set ALLOWTOPICCHANGE = RapGroup, StudentsComp617Group, RajB, MathiasRicken, JamesSasitorn^?