The papers are due by December 3 (in class).
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).
References
Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques 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.
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.
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.
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.
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.
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.
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
b = true
-----------------------------
if b then P else Q -tau-> P
b = false
-----------------------------
if b then P else Q -tau-> Q
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^(H(n)). P(n+1)where H(n) is the n-th element of the ordered sequence of Humming numbers.
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
b = true
-----------------------------
if b then P else Q -tau-> P
b = false
-----------------------------
if b then P else Q -tau-> Q
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.
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.