Work page for COMP 617

This page is used by students and instructors of COMP 617 to collaborate on selecting the papers that will be covered during the semester. It is consolidated at the start of each semester (first one or two weeks), and revisited at the end of each semester to collect comments for the next offering.

Course Description

COMP 617 provides educational modules to support research in the RAP group. The course has three goals:

1. To educate the student about a topic that you are interested in, and that fits in to the framework of our current research projects
2. To teach the student how to communicate these results both in writing and in presentation to other members of the research group. Of course, this also has the benefit of informing and educating other members of the group about your research and your research topic (this falls under the first point).
3. To teach the student about the processes of research, starting from reviewing related literature, finding an area to make a contribution, and hopefully, writing a paper documenting this contribution and communicating to the rest of the research community.

Research topics covered by the RAP group:

1. Advanced type systems (Concoqtion)
2. Physical Safe Computing (Acumen)
3. Hardware Description Languages (VPP)
4. Staging (Mint, MetaOCaml^?)
5. Compiling Dynamic Languages (Monty, Wolf, and Gradual Typing)

At the start of the semester, students are asked to think about the research that they would like to do this semester, and to explain the topic to me (the professor). Students are encouraged suggest research papers that they would like to cover. The best way to do this is probably to use google to search for things that come up when you enter key words associated with the research problem that you are interested in. Then you can forward pointers to these papers to me, along with a brief description of why you are interested in this paper. I will work with the students to select the papers that are will be serve the interests of the student and the RAP research program.

Significant communications by email take place to finalize the paper selection at the start of the semester. Please make sure that you subscribe to the class mailing list as soon as you sign up for the course. Scheduling of talks is usually finalized by the second week of class.

The course requires significant maturity on the part of the students. In particular, giving a presentation to a group of people is a significant responsibility. Scheduling a talk for COMP 517/617 means that the instructor and the students have committed their time to come and listen to you. They expect to learn new things from your talk, and in exchange they will give you feedback that will help you with your work and your presentation.

Grading Scheme

• 0% Completion of online course survey at the start of the semester.
  • This tends to give us a very good idea of the distribution of interest re the four core topics of our research.
  • It tends to give us many of the papers that we end up covering during the seminar.
  • The first time we did this we got a collection of twenty or so very good papers that were a big part of what we ended up picking.
  • This survey is an important mechanism for you to influence the direction of the seminar this semester.
• 10% Written proposal for you research during the semester. It is developed in two stages.
  • The first document is five hundred words, and needs to state clearly what research results you aim to establish during the semester, and what reference papers you will cover as background (due by second week)
  • The second document is about two pages long. This is your full proposal, and should 1) start with a brief statement of your overall research goal for the semester, 2) immediately follow that with 3 milestone achievements that you'd like to have during the semester, each corresponding to a talk (each of these milestones should be a research contribution intended for publication), and then 3) summaries for each of the three talks. Each should include title, reference papers (that I assume you will have read by that point), and an abstract of the talk itself. Make sure that these plans are consistent with the paper deadlines that you are working on. Make sure that this talk proposal is in the same document as the proposal you had sent me before (and probably revised a couple of times based on my input). It should be a PDF document.
• 10% List of at least four papers to be covered (due by second week)
• 20% Four talks (during the semester, due by the dates agreed on in first two weeks)
  • Speakers will have exactly the time 11:00-11:25 to talk, including answering any clarification questions.
  • Attendees will use the RAP talk feedback form to assess talk.
  • Continuation talks will be allowed. Make-up classes for now shows will be allowed, with 50% reduction in grade for that talk.
  • The time from 11:25-11:35 will be used for discussion questions.
  • Free discussion (11:35-11:40) while feedback is and reviewed.
  • Walid will give feedback (11:40-11:50)
  • The scribe will email Walid and Corky a pointer to the notes immediate after each class.
• 20% Written critiques of papers. There should be a critique of each paper your read. Three hundred words or less each (before each talk, post online). The critiques should followed the the RAP paper critique guidelines.
• 10% Powerpoint slides for talk (before each talk, post online)
• 10% Draft survey/tutorial on subject of choice. Two thousand words. (due by week seven)
• 10% Final survey/tutorial on subject of choice. Two thousand and fifty words. (due two weeks before finals)
  • If you have already written such a survey/tutorial for a previous 517/617, you may satisfy this requirement with a paper submission.
  • A paper submission would not be accepted unless you have already completed such a survey/tutorial for 517/617.
• 10% Participation on mailing lists, and in giving feedback to other participants. This will also include scribe duty.

All submissions should be handed in by posting them online. All documents should be wiki documents. All feedback will be provided online. All students are encouraged to give feedback on all submissions.

Occasionally, there will be guest lectures during the class.

Workload:

• Any student taking the course for credit reads at least four research papers and presents the material in four talks.
• Each lecture will have a scribe. Typically, you will need to scribe for 5-6 lectures.
• Students are required to attend at least one third of the lectures

If you are a graduate student working in the group, I would like you to sign up for the course and plan on giving four presentations. For this semester, I recommend that graduates sign up for the course as pass/fail.

If you are undergraduate student, you are encouraged to take the course as pass fail and to make one presentation in the course. You only need to attend about 30% of the meetings (the ones that relate to you research area). You are welcome to take the course for credit. In this case, you need to attend all class meetings, demonstrate your understanding of four research papers, and present four talks during the course.

In creating the schedule, we will also assigned different "topics" for the different days. For example, we may pick Mondays for dependent types and Wednesdays for mechanical modeling. This ways, students that are interested in only area know which days to attend.

Leftover ideas from previous years:

• Topics that our research group is interested in:
  • MSP for OO
    • Extensible parsing
    • Converge (Jun)
  • PSC: physical safety computing
    • Filipe Luiz's thesis (Angela)
    • Reasoning about stability
    • Reasoning about simulation
  • Concoction: indexed type
  • Theorem proving
  • device drivers
  • HWDL
    • Constraint solving: 1980 Nelson & Oppen (Jun?)
  • Functional MSP
    • Liang & Hudak & Jones
    • Monad transformer (Jun)
    • Monadic interpreter. (Jun)
  • compiling dynamic language
    • Dynamic typing with dependent types
  • DSLs broadly. Let me know if you are interested in a particular domain.
  • DSL for bioinformatics
  • Visual/graph-based language

Plan for Spring 2008 (Leftover plan from last year)

• Final selection: (please place links. Preceeding name is a suggestion for presenter)
  • (Corky) Scott's Notes on Domain Theory (as updated by Rebecca Parsons and Corky)
  • (Josh and Alex, special situation)
    • Will present four lectures each (eight total)
    • Four of the talks will be "Physical Modeling for Computer Scientists", relating Acumen and this course on dynamic modeling.
    • Other four talks will be developed jointly, and will be selected from the following:
    • Papes on bond-graphs and verification
    • Open hole tractor with tracks and modeling it in Acumen
  • Article on open hole tractors

• • (Cherif, Special situation)
    • Cherif is combinging his work outside the seminar with the seminar work and covering:
      • (Lecture 1)
        • Type inference with constrained types, Martin Sulzmann, Martin Odersky, and Martin Wehr, FOOL'97
        • Eliminating array bound checking through dependent types, Hongwei Xi and Frank Pfenning, PLDI'98
        • Papers mentioned in the related work section about Static analysis of array bounds checking from the paper Type-Assisted Dynamic Buffer Overflow Detection (pdf), SEC'02.
      • (Lecture 2)
        • Precise and efficient static array bound checking for large embedded C programs, PLDI'04
        • A practical inference and specializer for array bound checks elimination, Corneliu Popeea, Dana N. Xu, and Wei-Ngan Chin, PEPM'08
      • (Lecture 3)
        • Modular checking for buffer over-flows in the large, Brian Hackett, Manuvir Das, Daniel Wang,and ZheYang^?, ICSE '06
        • Concoqtion: Indexed types now!, Seth Fogarty, Emir Pasalic, Jeremy Siek, and Walid Taha, PEPM'07

• • (Greg L1) Dependently Typed Pattern Matching. Xi.
  • (Greg L2) Type Theory and Functional Programming. Kent Thompson
  • (Greg L3) LUSTRE: A declarative language for programming synchronous systems. Caspi, Pilaud, Halbwachs, Plaice (I can't find a non-acm version of this paper. I think that I'm going to look at the semantics of this language and how they deal with clocks, maybe for work with Uccello/VPP).
  • (Greg L4) A Realizability Model for Impredicative Hoare Type Theory. Morrisett

• • (Jun L1) A Monadic Approach for Avoiding Code Duplication when Staging Memoized Functions
  • (Jun L2) Floating-Point Error Analysis Based On Affine Arithmetic
  • (Jun L3) Toward Efficient Static Analysis of Finite-Precision Effects in DSP Applications via Affine Arithmetic Modeling
  • (Jun L4) MacQueen Plotkin and Sethi's paper on Types as Ideals

• • (Raj L1) Dependent types - Hongwei Xi
  • (Raj L2) Tag elimination
  • (Raj L3) Checking type safety of foreign function calls (PLDI 05)
  • (Raj L4) Survey of all related work for PhD^? thesis

Possible Guest Speakers:

• Someone from Cadence
• Someone from IBM
  • Andrew Martin
  • David Bacon
  • Roderic Rabbah
• Someone from Intel
  • Jim Grundy
  • John O'Leary
  • Bratin Saha
• Someone working on circuits
  • Markus Puschel
• Albert Cheng (Talk about scheduling and RT systems)
• Marcia O'Malley (Different approaches to physical modeling and robotics)
• Someone working on Bond Graphs?
• Paul Hudak to talk about FRP/Yampa
• Luis Calhords Cruz Filipe
• Greg Morrisett
• Hongwei Xi
• Dan Grossman
• Jens Palsberg
• Stephani Weirich
• Jeremy Siek - Gradual Typing
• Edward Lee
• Mary Sheeran
• [Who is doing constructive models of the reals?]

Left-over talks (for next semester)

• • McBride^?. "Dependently Typed Functional Programs and their Proofs"
  • Plotkin's paper on LCF Considered as a Programming Language
  • Milner's paper (or a newer equivalent) on a term model for ML

Left-over refs:

• 1,2,3,4
  • Coq book
• 2
  • Robotics book
  • Real analysis
  • http://www.ams.org/online_bks/mmono21/
• 3
  • Lava tutorial
• 4
  • A new tutorial by Walid
  • Ruby's manual
  • ACMEScript manual

Overview of research on 2

• The essential idea of type safey
  • Statically guaranteed properties
  • Todd's paper
• Constructive real-analysis
• Modeling mechnical systems
• Control theory
• Describing stability of mechanical systems
• Formal proofs about mechanical systems
• Ideas for DSLs capturing stable mechanical systems

Suggestions for Spring 2008

• Angela:
  • Edward Lee: On actor-oriented modeling and physical system simulation.
  • Paul Hudak: On their latest status about research in FRP and FHM(Functional Hybrid Modeling)
  • Greg Morrisett or Dan Grossman: certified compilers, proof-carrying code.
  • Abbas Edalat: Exact computation, Domain theoretical method for Differential Equations.
• Alex and Josh(?):
  • Four presentations entitled "Modeling for Computer Scientists" summarizing key ideas relating Acumen to this course on dynamic modeling.
  • Acumen modeling of an open hole tractor with tracks
  • Jan-Erik Strömberg et al: Switched Bond Graphs as Front-End to Formal Verification of Hybrid Systems
  • Simin Nadjm-Tehrani et al: Formal Verification of Dynamic Properties in an Aerospace Application
• Cherif:
  • A Gentle Introduction to Multi-stage Programming
  • Concoqtion: Indexed types now!
  • Brian Hackett, Manuvir Das, Daniel Wang,and ZheYang^?. Modular checking for buffer over-flows in the large, ICSE '06
  • Corneliu Popeea, Dana N. Xu, and Wei-Ngan Chin. A practical inference and specializer for array bound checks elimination. PEPM'08
  • Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types, PLDI'98
  • Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types, FOOL'97
• Gregory:
  • ...

Suggestions for Fall 2007

• Greg:
  • Type systems like the one in Concoqtion (indexed types?) (how they work, etc.)
  • Dynamically typed languages
  • Concurrency (with a look at compile-time analysis)
  • Proof carrying code (probably similar to concoqtion type system
  • ...

• Raj: It seems that the student opinions are split pretty evenly between theoretical topics and applications. I suggest that the course material reflect that distribution. Being a more applicative-type person myself, I think I'd enjoy it more if we could alternate between a theoretical topic and an example of its application.

• • Concurrency (Importance of programming languages in enabling concurrent programming, optimizations for improving concurrent behavior on multicore and other hardware)
  • Staging applications (State-of-the-art on staging real applications. How to stage your own application)
  • Staging and partial evaluation

• Walid: I suggest that we touch on topics such as:
  • Staged interpreters
  • Dynamically typed languages like Javascript. Here's a semantics
  • Gradual typing
  • Functional reactive programming
  • Device drivers and low-level programs

• Angela:
  • Paper reading and discussion: It will be nice to have some typical papers reviewed and discussed. We can then know what other people are doing and caring. Also, we can know what is good and what is bad when writing a paper.
  • Resource aware programming: How to model different kind of bounded resource and how to proof certain language is resource bounded.
• Joseph:
  • Calculus of constructions
  • Meta-theory behind MetaOCaml^?
  • More information behind the sort of proofs needed in PL papers. Last semester, we focused on implementing interesting constructs using dependent types. But, we never really discussed the sort of things we need to prove should we write a paper about a language that uses these tools. This includes proofs on both the type system and semantics of the language.
  • Differences between different kinds of dependent type systems. The typing rule for the dependent product is

E,Gamma|-A:s   E,Gamma::(a:A)|-B:s'
-----------------------------------
E,Gamma|-forall a:A,B:s''

• • The choice of s, s', and s'' radically affects the sort of things that we can express in our language. I believe that this classification is also known as the Barendregt cube.
• Cherif:
  • Multistage programing.
  • Object-Oriented Languages and the type theory behind them.
  • As an exercise: I suggest implementing more data structures and algorithms using Concoqtion.
  • Resource aware programming.
  • Decidability of a type system.

• Jun:
  • Comparison with other type/proof systems than coq/concoqtion, e.g. ATS, ACL2
  • Verification of concurrent programs (perhaps checking for some classes of race conditions? What's possible and what's not?)
  • Circuit generation from Concoqtion and proving its properties
  • How or can we avoid excessive wrapping or incurring runtime overhead just for the sake of verifying code (e.g. to apply verified sort to anything but snats, we need a wrapper that indexes the object with its rank within its ordering---with OCaml ints or floats, even that's not possible)

• In class discussion about future topics on April 20th
  • Error messages
  • Lambda cube
  • More guest lectures.
    • There is a guy from SLB want to come and talk about tools for finding bugs.
  • Measuring times
  • How does normalization work
    • Can we use more powerful reduction of Coq
  • DSL desing and implementation

• Bigger projects
  • Old projects on 617S07 webpage
  • Searching algorithms
  • DSL design and implementation.

Accommodations 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, AcumenGroup, StudentsComp617Group, RajB