The papers are due by December 7 (in class). This deadline is strict
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).
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-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.
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.
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.
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.
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.
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.
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.
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 corresponds to the 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.
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.
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.
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
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
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 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.
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
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.
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.
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.
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.
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.