EPSRC project Grant Number GR/L15685

Efficient Programming in Classical Logic

EPSRC project- Efficient Programming in Classical Logic

Post-Doctoral Researcher: Francois Monin

Value: 188.751 GBP

Duration: 1/December/1996-31/May/2000.

Collaborative sites: Cornell University, CWI, Nijmegen, Eindhoven.

Because of the powerful correspondence between proofs and types in constructive logic, such a logic has been almost always used as a foundation for both the theory and implementation of programming. Of the powerful systems based on constructive logic, we mention Nuprl, Coq, Lego, and Alf. However, decades of experience with these theorem proving and programming environment, have shown that constructive logic alone is not enough (e.g. Higman's lemma and the unbounded tableau search). For this reason, there is a comeback to classical logic as a foundation for programming. Working with classical logic however has both advantages and disadvantages. The advantages are that one can via the control operators have more efficient program extraction and theorem proving. The disadvantage is that normalisation or confluence and many other basic properties of programming might require special attention. For example, the Nuprl theorem prover is based on the constructive discipline of Martin-Lof which offers normalisation for free. When there was attempts to increase Nuprl with various control operators to improve its performance, normalisation was no longer free. The progress of Nuprl in the States was practical yet at the same time, work in the Netherlands on reduction strategies and on using weak normalisation as a way of showing strong normalisation was taking place by amongst others, Rob Nederpelt of the group of de Bruijn at Eindhoven and by Klop at CWI, Amsterdam.

The proposed project aims at studying classical logic as a foundation for programming without suffering from the usual disadvantages. This is particularly useful because classical logic (and proof by contradiction) is more understood than constructive logic, because constructive logic has been shown to be insufficient by years of experience with constructive systems, because classical logic is more efficient as one does not have to find a particular witness and hence many calculations can be avoided. In fact, the people who are returning to classical logic are precisely those people who have been defending constructive logic for the last 25 years. This area has now sparked the attention of many researchers in the world and still has many open problems (such as normalisation, typing control operators, finding the reduction strategy which will make sense for a control operator, and so on). We offer to study this area from both the theoretical and practical sides. Here is a one page summary.

JOURNAL PAPERS

1. Fairouz Kamareddine and Twan Laan (2001),
   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 ?, 2001, Kluwer Academic Publishers.

2. Fairouz Kamareddine (2000)
   Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction
   Logic and Computation volume 10 (5), pages 721-738, 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.
   Special issue in the Journal of Logic and Computation volume 10 (3), pages 349-380, 2000, Oxford University Press.

4. 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.

5. 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 no. 6(6), pages 843--874, 1998, ISSN 0945-9103, Oxford University Press.

6. 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.

7. 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)

8. 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, editor (2001)
   Special issue on type and set theoretical foundations of Computation.
   Special issue in the Journal of Logic and Computation volume 11 (3), 2001, Oxford University Press.

2. Fairouz Kamareddine, editor (2001)
   Special issue on rewriting and theorem proving.
   Special issue in the Logic Journal of the Interest Group of Pure and Applied Logic ( Log. J. IGPL), 2001.

3. 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,
   ACM publications 1-58113-265-4/00/0009, Pages 163-174, 2000.
   Here are the slides of the talk.

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

3. Fairouz Kamareddine and Francois Monin (1999)
   On Automating Inductive and Non-Inductive Termination Methods
   Asian Computing Science Conference, ASIAN'99,
   Lecture Notes in Computer Science 1742, Pages 177-189, ©Springer-Verlag, 1999.

4. Fairouz Kamareddine and Francois Monin (1999)
   On Formalised Proofs of Termination of Recursive Functions
   Lecture Notes in Computer Science 1702, Pages 29-46,
   International Conference on Principles and Practice of Declarative Programming, PPDP'99, ©Springer-Verlag, 1999.

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

6. 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: