EPSRC project grant Number GR/K25014

Advantages of a new lambda-notation

EPSRC project- Theoretical and Implementation advantages of a new lambda notation

Principal investigator: Fairouz Kamareddine

Post-Doctoral Researcher: Alejandro Rios

Value 138.507 GBP

Duration: 1/October/1994-30/September/1997.

Objectives

The first main objective of this project is to study the advantages of lambda calculi written in the style of de Bruijn's famous Automath, to investigate extending these calculi with concepts (such as explicit definitions and substitutions, generalised reductions and new notions of typing) that are vital for efficient implementation and theorem proving, and to study the theoretical properties of such extended calculi. The second main objective (providing a common framework for logic and functional programming) can only be studied once efficient calculi have been identified.

Progress

Under this proposal, we made vital progress in objective 1 and a good start on objective 2. We provided a thorough study of calculi extended with the above mentioned concepts, established the essential theoretical properties of these calculi and have implemented many of them studying the behaviour of program evaluation and lengths of proofs under these concepts. We also made a new and useful step in the study of theorem proving and of $\lambda$-calculi that bridge theory and implementation in FP, LP and TP. A PhD student Richard Reid made a nice tool with a user interface that implements calculi and extensions we (under this project) and others studied in recent years.

The papers published under this grant consist of:

Journals: [2, 3, 5, 6, 10, 11, 12, 13, 14, 18, 19]
Conferences:[1 9 15 17]
Submitted: [4,7,8,16,20,21]

This grant also led to first International school on type theory and term rewriting and the first workshop on explicit substitutions . This grant also resulted in many collaborations with Holland, France and the US (see projects/ ) and to new EPSRC grants GR/L15685 Efficient Programming in Classical Logic and GR/L36963 On Type Theory and Term Rewriting for Efficient and Expressive Programming Languages

References

[1] Barthe, Kamareddine and Rios, Explicit substitutions for the $\lambda \Delta$-calculus, ALP-HOA'97, volume 1298 of LNCS, '97.

[2] Bloo, Kamareddine and Nederpelt, The Barendregt Cube with Definitions and Generalised Reduction , Journal of Information and Computation 126(2), 123-143, 1996.

[3] Curien, Hardin, and Rios, Strong Normalization of Substitutions, Logic and Computation, 6, '96.

[4] Kamareddine A semantics for step-wise substitution and reduction, submitted.

[5] Kamareddine Type Theory, Collective, Distributive Predication , Logic, Language and Information, 4({2}):85--109, 1995.

[6] Kamareddine Important Issues in Foundational Formalisms, Journal of Interest Group of Pure and Applied Logic 3({(2,3)}):291--317, 1995.

[7] Kamareddine A Reduction Relation for which Postponement of {K}-Contractions, Conservation and Preservation of {SN} Hold, submitted, '96.

[8] Kamareddine, Bloo, and Nederpelt. Definitions, $\Pi$-conversion in Type Theory. submitted, '95.

[9] Kamareddine, Bloo, and Nederpelt, Classes which Approximate Reductional $\equiv$, CSL'97, '97.

[10] Kamareddine and Laan, A reflection on Russell's Ramified Types and Kripke's Hierarchy of Truths, Journal of Interest Group of Pure and Applied Logic 4(2), 195-213, 1996.

[11] Kamareddine and Laan, A Correspondance between Nuprl, the Ramified Theory of Types and Pure Type Systems , Submitted.

[12] Kamareddine and Nederpelt, Refining reduction in the lambda calculus, Journal of Functional Programming 5(4), 637-651, 1995.

[13] Kamareddine and Nederpelt. A Useful $\lambda$-Notation, Theoretical Computer Science, 155:85--109, '96.

[14] Kamareddine and Nederpelt, Canonical Typing and Pi-reduction in the Barendregt Cube, Journal of Functional Programming 6(2), 245-267, 1996.

[15] Kamareddine and Rios, A lambda calculus `a la de Bruijn with explicit substitutions , PLILP'95, LNCS 982, 45-62, 1995.

[16] Kamareddine and Rios, Bridging de {Bruijn} indices and variables names in explicit substitutions calculi, submitted, '96.

[17] Kamareddine and Rios, Generalised beta-Reduction and Explicit Substitutions, PLILP'96, LNCS 1140, 378-392, 1996.

[18] Kamareddine and Rios, Extending a lambda calculus with explicit substitution which preserves Strong Normalisation into a confluent calculus on open terms, Journal of Functional Programming 7(4), 1997.

[19] Kamareddine, Rios and Wells Calculi of Generalised beta-reduction and Explicit Substitutions: The Type Free and Simply Typed Versions, Journal of Functional and Logic Programming, 1998.

[20] Kamareddine and Rios, Efficiency of $\lambda$-calculi, submitted.

[21] Kamareddine and Rios. Bridging the $\lambda \sigma$- and $\lambda s$-Styles of Explicit Substitutions, Submitted.

Maintained by Fairouz Kamareddine