A second-order pattern matching algorithm for the cube of typed λ-calculi

1. H. Barendregt, Introduction to Generalized Type Systems, To appear in Journal of Functional Programming.

   Google Scholar 

2. Th. Coquand, Une Théorie des Constructions, Thèse de troisième cycle, Université Paris VII, 1985.

   Google Scholar 

3. Th. Coquand, An analysis of Girard's paradox, Proceedings of Logic in Computer Science, 1986, pp. 227–236.

   Google Scholar 

4. Th. Coquand, G. Huet, The Calculus of Constructions, Information and Computation, 76, 1988, pp. 95–120.

   Google Scholar 

5. Th. Coquand. J. Gallier, A Proof of Strong Normalization For the Theory of Constructions Using a Kripke-Like Interpretation, Personal communication.

   Google Scholar 

6. G. Dowek, L'Indécidabilité du Filtrage du Troisième Ordre dans les Calculs avec Types Dépendants ou Constructeurs de Types (The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors), Compte Rendu à l'Académie des Sciences, 1991.

   Google Scholar 

7. G. Dowek, The Undecidability of Pattern Matching in Polymorphic λ-Calculus, In preparation.

   Google Scholar 

8. G. Dowek, A Second-Order Pattern Matching Algorithm for the Cube of typed λ-Calculi, Rapport de Recherche INRIA, 1991.

   Google Scholar 

9. C. M. Elliott, Higher-order Unification with Dependent Function Types, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, N. Dershowitz (Ed.), Lecture Notes in Computer Science, 355, Springer-Verlag, 1989, pp.121–136.

   Google Scholar 

10. C. M. Elliott, Extensions and Applications of Higher-order Unification, PhD Thesis, 1990, Carnegie Mellon University, Pittsburgh, Report CMU-CS-90-134.

    Google Scholar 

11. J. Gallier, On Girard's Candidats de Réductibilité, Logic and Computer Science, P. Odifreddi (Ed.), Academic Press, London, 1990, pp. 123–203.

    Google Scholar 

12. H. Geuvers, M.J. Nederhof, A Modular Proof of Strong Normalization for the Calculus of Constructions, Catholic University Nijmegen.

    Google Scholar 

13. J.Y. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de Doctorat d'État, Université de Paris VII, 1972.

    Google Scholar 

14. R. Harper, F. Honsell, G. Plotkin, A Framework for Defining Logics, Proceedings of Logic in Computer Science, 1987, pp. 194–204.

    Google Scholar 

15. G. Huet, A Unification Algorithm for Typed λ-calculus, Theoretical Computer Science, 1, 1975, pp. 27–57.

    Google Scholar 

16. G. Huet, Résolution d'Équations dans les Langages d'Ordre 1,2, ..., ω, Thèse de Doctorat d'état, Université de Paris VII, 1976.

    Google Scholar 

17. G. Huet, B. Lang, Proving and Applying Program Transformations Expressed with Second Order Patterns, Acta Informatica, 1978, 11, pp. 31–55.

    Google Scholar 

18. D.A. Miller, Unification Under a Mixed Prefix, To appear in Journal of Symbolic Computation.

    Google Scholar 

19. F. Pfenning, Unification and anti-Unification in the Calculus of Constructions, To appear in Proceedings of Logic in Computer Science, 1991.

    Google Scholar 

20. D. Pym, Proof, Search and Computation in General Logic, PhD thesis, University of Edinburgh. Report CST-69-90 also ECS-LFCS-90-125.

    Google Scholar 

21. J.A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the Association for Computing Machinery, 12, 1, 1965, pp. 23–41.

    Google Scholar 

22. A. Salvesen, The Church-Rosser Theorem for LF with β/ν-reduction, Manuscript, University of Edinburgh, 1989.

    Google Scholar 

Download references