|
|
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:
- To educate the student about a topic that you are interested in, and that fits in to the framework of our current research projects
- 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).
- 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:
- Advanced type systems (Concoqtion)
- Physical Safe Computing (Acumen)
- Hardware Description Languages (VPP)
- Staging (Mint, MetaOCaml?)
- 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. 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 survey on subject. Five hundred words. (due by second week)
- 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 10:00-10:25 to talk, including answering any questions.
- 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 10:25-10:50 will be used for discussion.
- The scribe will email Walid and Corky a pointer to the notes immediate after each class.
- 20% Written summaries of papers. There should be a summary of each paper your read. Three hundred words or less each (before each talk, post online)
- 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
- 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)
- Article on open hole tractors
-
- (Cherif, Special situation)
- Cherif is combinging his work outside the seminar with the seminar work and covering:
- (Lecture 1)
- (Lecture 2)
- (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
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
- 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
- 2
- 3
- 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(?):
- 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)
Teaching.617WishList moved from Teaching.617Next on 21 Nov 2007 - 15:41 by WalidTaha - put it back
|
Show attachments
Hide attachments
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.