EPSRC project GR/L36963

On Type Theory and Term Rewriting for Expressive and Efficient Programming Languages

EPSRC project- On Type Theory and Term Rewriting for Expressive and Efficient Programming Languages

Post-Doctoral Researcher: Joe Wells

Value 234,979 GBP

Duration: 1/March/1997-30/April/2000

Here is the one page summary.

Objectives

Of course, TT and TR have not solved all problems of programming languages, and recent work has illuminated interesting areas for further research. One example is the goal of combining expressive type systems with automated type inference (ATI). Milner's successful language ML supports ATI, but its type system has limitations on polymorphic types making some code reuse more difficult and its module system is awkwardly separate. Expressive type systems such as F, F<, Feta, and Fomega have the potential to solve ML's difficulties. Unfortunately, these systems have fatal problems with ATI. Dr. Wells recently showed ATI impossible for F and Feta, Urzyczyn showed the same for Fomega, and Pierce showed F<'s subtyping to be undecidable. As a result, an open issue is discovering a type system expressive enough to overcome ML's limitations while allowing ATI. A related open issue is to characterize ML or a similar language in its entirety in a theoretically elegant manner, as opposed to the awkward ad hoc combinations used until now.

Another example of an interesting area for further research is in the combination of TT and TR. Since most TT research is based on typed lambda-calculi while TR better describes what implementations actually do, there is a conceptual gap between most TT research and its application in programming languages. One way of bridging this gap is explicit substitution, where lambda-calculus operations are implemented by an underlying TR system. Many problems remain open, most especially combining explicit substitution with reasonably expressive type systems. Another way of bridging the gap between TT and TR is to formulate typed term rewriting systems directly, bypassing the lambda-calculus. Preliminary research indicates this is a viable approach, but leaves as an open issue the extension to type systems expressive enough to handle the problems of modern programming languages.

Based on the above reasoning, our specific goals are:

1. Expanding boundaries of type system expressiveness without losing ATI.
2. Formalising a language like ML in a general yet simple framework, e.g., the framework of a pure type system (PTS).
3. Combining these results in a language partially or entirely based on explicit concepts of TR.

Under this proposal, we made vital progress on all objectives. We have thoroughly studied programming language calculi using explicit rewriting concepts, established the essential theoretical properties of these calculi, and carried out prototype implementations. Our achievements answer in extreme thoroughness and depth to our three objectives. We have also made new and useful steps in the study of calculi that bridge theory and implementation. The progress of this project has been directed by the work of Dr. Wells on solving open problems in the field, e.g., decidability of typing of systems like F and the work of Prof. Kamareddine on formalising type systems using explicit rewriting.

Under this grant, we published 11 journal articles, 11 conference articles, 1 special journal issue and have 7 submitted articles. We have also initiated two international workshops:

1. The First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs: WESTAPP '98 .
2. The First International Workshop on Intersection Types and Related Systems (ITRS '00).

JOURNAL PAPERS

1. Fairouz Kamareddine and Twan Laan (2000),
   A Correspondence between Martin-Loef Type Theory, the Ramified Theory of Types and Pure Type Systems
   Logic, Language and Information (J. Logic Lang. Inform.) volume ? Number?, pages ?, 2000, Kluwer Academic Publishers.

2. Fairouz Kamareddine (2000)
   Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction
   Logic and Computation volume 10 (5) pages ??, 2000, Oxford University Press.

3. Fairouz Kamareddine and Alejandro Rios (2000)
   Relating the Lambda-sigma and Lambda-s styles of Explicit Substitutions
   Special issue on Type Theory and Term Rewriting: a collection of papers.
   Special issue in the Journal of Logic and computation, 10 (3), 2000, Oxford University Press.

4. Rene Vestergaard and J.B.Wells (??)
   Cut rules and explicit substitutions
   Mathematical Structures in Computer Science, volume =??, pages ??, year??. To appear.

5. J.B.Wells,
   Typability and type checking in System F are equivalent and undecidable
   Annals of Pure and Applied Logics, volume 98, 1999

6. J.B.Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak,
   A calculus with polymorphic and polyvariant flow types.
   J. Funct. Prog., 199X. Accepted subject to revisions.

7. Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1999)
   On $\Pi$-conversion in The $lambda$-cube and the combination with abbreviations
   Annal of Pure and Applied Logics, volume 97, no. 1-3, pages 27--45, 1999, Elsevier, North-Holland.

8. Fairouz Kamareddine and Alejandro Rios (1998)
   Bridging de Bruijn indices and variable names in explicit substitutions calculi
   the Logic Journal of the Interest Group of Pure and Applied Logic ( Log. J. IGPL) no. 6(6), pages 843--874, 1998, ISSN 0945-9103, Oxford University Press. Primary Classification 03B40

9. Fairouz Kamareddine (1998)
   The Soundness of Explicit Substitution with Nameless Variables
   International Journal of Foundations of Computer Science 9(3), pages 321-349, 1998, World-Scientific Publishing Company.

10. Fairouz Kamareddine, Alejandro Rios and Joe Wells (1998)
    Calculi of Generalised $\beta$-Reduction and Explicit Substitutions: The Type free and Simply Typed Versions Journal of Functional and Logic Programming, ( JFLP) Volume 1998, article 5, pages 1--44, ISSN 1080-5230, MIT Press, 4 June 1998. Primary Classification 03B40 (68N15)

11. Fairouz Kamareddine and Alejandro Rios (1997)
    Extending a $\lambda$-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
    Journal of Functional Programming (J. Funct. Programming) volume 7, no. (4), pages 395--420, 1997, Cambridge University Press. Primary Classification 03B40 (68N15 68Q42)

EDITED VOLUMES

1. Fairouz Kamareddine and Jan Willem Klop, editors (2000)
   Special issue on Type Theory and Term Rewriting: a collection of papers.
   Special issue in the Journal of Logic and Computation volume 10 (3), 2000, Oxford University Press.

CONFERENCE PAPERS

1. Mauricio Ayala and Fairouz Kamareddine (2000)
   Higher Order Unification via lambda se-Style of Explicit Substitution
   International Conference on Principles and Practice of Declarative Programming, PPDP'00,
   Lecture Notes in Computer Science ?, Pages ?, ©Springer-Verlag, 2000.

2. Mauricio Ayala and Fairouz Kamareddine (2000)
   Strategies for Simple-Typed Higher Order Unification via lambda se Style of Explicit Substitution.
   In the Third Int'l Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, A Satellite workshop of RTA 2000, Norwich, UK, 2000.

3. J.B.Wells and Rene Vestergaard (2000)
   Equational reasoning for linking with first-class primitive modules.
   In Proc. European Symp. on Programming. LNCS. ©Springer-Verlag, 2000.

4. Assaf J. Kfoury and J.B.Wells
   Principality and decidable type inference for finite-rank intersection types
   In Conf. Rec. POPL '99: 26th ACM Symp. Principles of Prog. Languages, 1999.

5. Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, and J.B.Wells
   Relating typability and expressibility in finite-rank intersection type systems
   In Proc. 1999 Int'l Conf. Functional Programming, 1999.

6. Rene Vestergaard and J.B.Wells
   Cut rules and explicit substitutions
   In Second Int'l Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, Trento, Italy, 5 July 1999

7. J.B.Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak.
   A typed intermediate language for flow-directed compilation.
   In Proc. 7th Int'l Joint Conf. Theory & Practice of Software Development, 1997.

8. Allyn Dimock, Robert Muller, Franklyn Turbak, andJ.B.Wells,
   Strongly typed flow-directed representation transformations
   In Proc. 1997 Int'l Conf. Functional Programming, 1997.

9. Franklyn Turbak, Allyn Dimock, Robert Muller, and J.B.Wells,
   Compiling with polymorphic and polyvariant flow types.
   In First Int'l Workshop on Types in Compilation, June 1997.

10. Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1997)
    An Approximation of Reductional Equivalence
    Computer Science Logic, CSL'97, Aarhus.

11. Gilles Barthe, Fairouz Kamareddine and Alejandro Rios (1997)
    Explicit substitutions for the $\lambda \Delta$ calculus 6th international joint conference on Algebraic and Logic Programming and Higher Order Algebra, ALP-HOA'97,
    Lecture Notes in Computer Science 1298, Pages 209-223, ©Springer-Verlag, 1997.

Workshops/events organised under this grant: