Fall 99, CSE 520: Projects

Projects

There are three kinds of projects: In all the cases, the project consists in writing an individual report. The paper should be written as if it was meant for publication, i.e. to be read by other students / researchers.

The papers are due by December 7 (in class). This deadline is strict

I. Overview projects

An overview paper should consists of an introductory tutorial on a subject related to the course, and should be 10-15 pages long. It should contain the following parts:
  1. Motivations
  2. History / Literature
  3. Main definitions
  4. Main results
  5. Implementations (if applicable)
  6. Applications / relevance for computer science
  7. Open problems
The criteria of evaluation will be the standard criteria that apply for publication of overview papers, namely:
  1. Organization and structure
  2. Clarity
  3. Focus on the relevant definitions and results
Furthermore, initiave in searching for other reference material relevant for the subject (besides the material suggested by me) will be highly appeciated.

II. Implementation projects

A project of this kind consists in writing a program for solving some specific problem related to the subjects of the course. The program should be well documented and there should be some text explaining the problem, and specifying the solution. More precisely, the report should contain the following parts:
  1. Explanation of the problem, motivations and relevant literature
  2. Technical preliminaries (existing in literature)
  3. Additional technical definitions, if necessary (developed by the student)
  4. Specification of the solution (developed by the student)
  5. Code of the program (developed by the student)
  6. Open problems
The criteria of evaluation will be:
  1. Organization, structure
  2. Clarity
  3. Correctness of the program

III. Research projects

A research project should focus on solving some technical problem (typically, proving some technical result) on a subject related to the course. It should contain the following parts:
  1. Explanation of the problem, motivations and relevant literature
  2. Technical preliminaries (existing in literature)
  3. Additional technical definitions, if necessary (developed by the student)
  4. Solution of the problem / technical results, with proofs (developed by the student)
  5. Open problems
The criteria of evaluation will be:
  1. Organization and structure
  2. Clarity
  3. Correctness of results

List of subjects for projects

This list is not complete. New suggestions will be added during the lectures on concurrency. Students are welcome to come out themselves with ideas for projects, subject to my approval.

For each subject a list of relevant works is given. This should be interpreted as a minimum reference material. Students are encouraged to search themselves for other reference material relevant for the subject (one way to start is to look at the list of references at the end of the papers).

I. Overview projects

  1. Explicit substitutions

    The foundations of reduction using "environments" (explicit substitutions) instead of substitutions. Link between theory and implementation. Convenient tool for reasoning about functional languages and their implementations.

    Initiated by Nadathur and independently by Abadi, Cardelli, Levy, and Curien.

    References

    Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean,Jac˝uew Levy. Explicit Substititions. Journal of Functional Programming 1, 4 (October 1991), 375-416.

    Gopalan Nadathur and Debra Sue Wilson. A Notation for Lambda Terms: A Generalization of Environments. To appear in Theoretical Computer Science 198(1-2): 49-98, 1998.

    Gopalan Nadathur. An Explicit Substitution Notation in a lambda Prolog Implementation. Technical Report. University of Chicago. December 1997.

  2. The polymorphic lambda calculus

    The idea is to consider as types the formulae of the second order propositional calculus. In particular, types can contain universal quantifiers on type variables. For instance the identity function \x.x has type (forall A. A -> A). In this way, it is possible to write terms where the same functions is applied to different types.

    Some languages, like ML, adopt a weak form of polymorphism, where the quantification can be only at the top level (let polimorphism). The advantage of this restriction is that it makes typeability decidable.

    References

    Henk P. Barendregt. Lambda Calculi with types. Chapter in the Handbook of Logic in Computer Science, Vol. 2. S. Abramski, Dov M. Gabbay, and T.S.E. Maibaum, Eds. Oxford Science Publications, 1992.

    J. C. Reynolds. Towards a theory of type structure. In Ehrig et al., editor, Mathematical Foundations of Software Development, volume 19 of Lecture notes in Computer Science, pages 408-425. Springer. 1974.

  3. Logical Frameworks

    Dependent Types. The idea is to consider as types the formulae of the predicate calculus. Following the Curry-Howard analogy, terms are then interpreted as representant of proofs possibly depending on other proofs.

    References

    Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.

    Henk P. Barendregt. Lambda Calculi with types. Chapter in the Handbook of Logic in Computer Science, Vol. 2. S. Abramski, Dov M. Gabbay, and T.S.E. Maibaum, Eds. Oxford Science Publications, 1992.

    Papers on ELF. See Frank Pfenning's home page at CMU.

  4. Recursive types

    A "minimum fixpoint" operator mu is introduced on types. So for instance it is possible to define the type (A list) as muX(1 + A * X). In this system it is possible to define infinite types, and in this way also terms like \x.x x have a type: muX(X -> A).

    References

    Glynn Winskel. The Formal Semantics of Programming Langauges The MIT Press, 1993.

    Henk P. Barendregt. Lambda Calculi with types. Chapter in the Handbook of Logic in Computer Science, Vol. 2. S. Abramski, Dov M. Gabbay, and T.S.E. Maibaum, Eds. Oxford Science Publications, 1992.

  5. The Calculus of Constructions

    Dependent higher-order types. Types as formulas of the Higher Order predicate calculus. (See also the Lambda-Cube, Barendregt)

    References

    Th. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:95-120, 1988.

    Henk P. Barendregt. Lambda Calculi with types. Chapter in the Handbook of Logic in Computer Science, Vol. 2. S. Abramski, Dov M. Gabbay, and T.S.E. Maibaum, Eds. Oxford Science Publications, 1992.

    Note: all these type systems are explained in a systematic way in the book chapter of Barendregt ("Lambda calculi with types). An interesting project would be to make a comparative analysis of all of them, focusing on their properties like decidability of typing, subject-reducion theorem, etc.

  6. Adding Polymorphic types to Java There are several proposals to enhance Java with generic polymorphism. One of the most promising attempts if the language Generic Java, developed by Martin Oderski and Philip Wadler.

    References

    Making the future safe for the past: Adding Genericity to the Java Programming Language, Gilad Bracha, Martin Odersky, David Stoutamire and Philip Wadler. Proc. OOPSLA'98

    Pizza into Java: Translating theory into practice, Martin Odersky and Philip Wadler. Proc. 24th ACM Symposium on Principles of Programming Languages, Paris, France, January 1997.

    Two Ways to Bake Your Pizza - Translating Parameterised Types into Java, Martin Odersky, Enno Runne, and Philip Wadler. Generic Programming - Proceedings of a Dagstuhl Seminar, Springer Lecture Notes in Computer Science 1766. Copyright © Springer Verlag.

  7. Higher-order unification

    The theory of unification which is at the basis of Lambda Prolog (and other logical higher-order languages like ELF).

    References

    Gerard Huet, A Unification Algorithm for Typed lambda-Calculus, Theoretical Computer Science 1:27-57, 1973.

    W. Snyder and J. Gallier, Higher-Order Unification Revisited: Complete Sets of Transformations, Journal of Symbolic Computation 8: 101 - 140, 1989.

  8. Decidability of bisimulation

    Bisimulation can be easily shown to be decidable for finite-state processes (i.e. processes whose transition graph is finite). In general, bisimulation is not decidable for infinite-state processes. However, recent research has identified some classes of infinite-states processes where bisimulation is still decidable. One of these classes correspoţds t/ tje context-free grammars (in Greibach Normal Form). The decidability of bisimulation in this case is particularly surprising, because it is well-known that language equivalence (= trace equivalence) for context-free grammars is undecidable.

    References

    Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. Journal of the Association for Computing Machinery 40(3): 653-682, 1993.

    Hans Hüttel and Colin Stirling. Actions speak louder than words: Proving bisimilarity for context-free processes. Journal of Logic and Computation, 8(4):485-509, August 1998. (A previous version of this paper appeared in Proceedings of LICS 91.)

    S°ren Christensen, Hans Hüttel and Colin Stirling. Bisimilarity is Decidable for All Context-Free Processes. Information and Computation, 121(2):141-148, September 1995. (A previous version of this paper appeared in Proceedings of CONCUR 92.)

    Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decidable subsets of CCS. The Computer Journal, 37(4):233-242, 1994.

    Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 386-396, Montreal, Canada, 19-23 June 1993. IEEE Computer Society Press.

  9. Bisimulation as a congruence

    Bisimulation is a general notion which can be applied to any language whose semantics is specified via a transition system. One of the properties which are very desirable for any kind of equivalence considered for verification, is the property of being a congruence. Recent research has pointed out the conditions (on the rules of the transition system) which guarrantee that the associated bisimulation equivalence is a congruence. Furthermore, a complete set of axioms (for bisimulation congruence) can be derived automatically.

    References

    J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992.

    L. Aceto, B. Bloom and F.W. Vaandrager. Turning SOS rules into equations. LICS'92 Special Issue of Information and Computation, 111(1):1-52, 1994.

II. Implementation projects

  1. Implementation of a type-inference system for the extension of the lambda calculus presented in Lecture 14

    The program should implement the function "type of M". I.e., given a PCF term M, the function should return its most general type.

    You can choose any implementation language you want among the followings: Lambda Prolog, Prolog, ML, C++ or Java. These languages are listed in order of suitableness for solving the problem: Lambda Prolog is the most suitable, C++ and Java are the least suitable. The reason is that Lambda Prolog, Polog and ML allow constructs for symbolic manipulation (data types and data terms). Lambda Prolog and Prolog have unification as a primitive. Lambda Prolog has a way of representing abstractions directly in the language.

  2. Implementation of the type-inference system of PCF
  3. Implementation of a type-inference system for ``PCF with let polymorphism'' in lambda Prolog

    Let polymorphism, or weak polymorphism, is a restricted form of polymorphism which allows expressions like

       let f = \x.x 
        in 
           if (f true) then (f 1) else (f 2)
    
    to be typeable. It is used for instance in ML.

    Ask the instructor for references on the let polymorphism

  4. The Hamming sequence

    This project consists in specifying and implementing a system generating the ordered sequence (without repetitions) of the Hammming numbers. A Humming number is any number of the form 2k3m5n for arbitrary k, m, and n. The specification should be given in CCS or in pi-calculus, and the implementation should be done in Java.

    The CCS (or pi-calculus) definition should express the system as a parallel composition of (at least) the following processes:

    You can find a description of this design also at pag. 286 of the book

    Chris Reade. Elements of Functional Programming. Addison-Wesley, 1989.
    Note that the implementation of the system proposed in this textbook is sequential. Hence: don't follow that implementation!

    In the specification, you can use CCS or pi-calculus enriched with

    It is preferable to have the above processes communicating with each other via queues. (This will allow the processes to be more independent, i.e. will allow more parallelism.) A queue can be specified in CCS or in pi-calculus in the same way as a buffer with unbounded capacity. Note that also these queues, in the CCS (or pi-calculus) specification, will be processes.

    The Java implementation should follow the CCS (or pi-calculus) design, using threads to implement processes. There should be a thread for each of the processes described in the CCS (or pi-calculus) specification, except for queues: you can implement queues as passive objects if you prefer. Note that in this case the methods of the queues should be synchronized.
    Note: There are testbooks presenting C++ or Java programs solving this problem in various fashions. Therefore, a solution containing only the Java implementation, or in which the Java implementation does not correspond to the CCS (or pi-calculus) specification, will be considered absolutely insufficient.

    It is not strictly requested to prove the correcteness of the CCS (or pi-calculus) specification, but it would be appreciated (in a concrete way, i.e. it will contribute to the final grade). The correctness consists in proving that the system is (weakly) bisimilar to the process P(1), where P(n) is defined inductively as follows:

    P(n) = out^(H(n)). P(n+1)
    where H(n) is the n-th element of the ordered sequence of Humming numbers.

  5. The Heratosthenes' Sieve

    This project is analogous to the previous one and consists in specifying and implementing a system, based on Eratosthenes' sieve method, for generating the ordered sequence of the prime numbers (starting from 2). The specification should be given in CCS or in pi-calculus, and the implementation should be done in Java.

    The CCS (or pi-calculus) definition should express the system as a parallel composition of (at least) the following processes:

    You can find a description of this design also at pag. 274 of the book

    Ravi Sethi. Programming Languages Concepts and Constructs. 2nd edition, Addison-Wesley, 1996.
    Note that the implementation of the system proposed in this textbook is sequential. Hence: don't follow that implementation!

    In the specification, you can use CCS or pi-calculus enriched with

    It is preferable to have the above processes communicating with each other via queues. (This will allow the processes to be more independent, i.e. will allow more parallelism.) A queue can be specified in CCS (or in pi-calculus) in the same way as a buffer with unbounded capacity. Note that also these queues, in the CCS (or pi-calculus) specification, will be processes.

    The Java implementation should follow the CCS (or pi-calculus) design, using threads to implement processes. There should be a thread for each of the processes described in the CCS (or pi-calculus) specification, except for queues: you can implement queues as passive objects if you prefer. Note that in this case the methods of the queues should be synchronized.
    Note: There are testbooks presenting CC++ or Java programs solving this problem in various fashions. Therefore, a solution containing only the Java implementation, or in which the Java implementation does not correspond to the CCS (or pi-calculus) specification, will be considered absolutely insufficient.

    It is not strictly requested to prove the correcteness of the CCS (or pi-calculus) specification, but it would be appreciated (in a concrete way, i.e. it will contribute to the final grade). The correctness consists in proving that the system is (weakly) bisimilar to the process P(1), where P(n) is defined inductively as follows:

    P(n) = out^(F(n)). P(n+1)
    where F(n) is the n-th prime number starting from 2.

  6. An interpreter for the pi-calculus

    This project consists in defining in lambda Prolog a prototype interpreter for the pi-calculus. More specifically, the interpreter should emulate (obviously in a sequential fashion) the transition relation of the pi-calculus, i.e. the lambda Prolog program should contain the definition of a predicate trans : Proc -> Act -> Proc -> o such that (trans P alpha Q) holds if and only if there is a alpha-transition from P to Q (in the operational semantics of the pi-calculus). You can define also other variants of this relation if convenient.

  7. A theory for asynchronous communication
    This project consists in investigating the theory of testing semantics for the calculus of asynchronous communication presented in
    Frank S. de Boer, Jan Willem Klop, and Catuscia Palamidessi. Asynchronous communication in process algebra. In Proc. of the seventh annual IEEE symposium on Logics in Computer Science (LICS), pages 137-147. IEEE Computer Society Press, Los Alamitos, California, 1992.
    This is a "fresh topic": the theories which have been investigated so far for this calculus are relative to trace, bisimulation and failure set semantics, but not testing.

    If you are interested in this project please contact me for reference material about testing semantics.

III. Research projects

  1. Strong Normalization theorem for the extension of the lambda calculus presented in Lecture 14

    The project consists in proving that the language presented in Lecture 14 enjoys the following property: if M is typeable, then M is strongly normalizing.

    The proof can be based on the corresponding proof for the simply typed lambda calculus, which can be found in the chapter book by Barendregt (Section 4.3):

    Henk P. Barendregt. Lambda Calculi with types. Chapter in the Handbook of Logic in Computer Science, Vol. 2. S. Abramski, Dov M. Gabbay, and T.S.E. Maibaum, Eds. Oxford Science Publications, 1992.

  2. Subject-reduction theorem for PCF

    The project consists in showing that the language PCF enjoys the subject-reduction theorem, i.e. if M : T and M evaluates to N, then N : T.