Références

[ACCL90]

M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. In Proc. 17th ACM Symp. on Principles of Programming Languages, pages 31–46, San Francisco, 1990.

[Art97]

T. Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Universiteit Utrecht, 1997.

[Aug85]

L. Augustsson. Compiling pattern matching. In Functional Programming Languages and Computer Architecture, Nancy, LNCS 201. Springer-Verlag, September 1985.

[Bar84]

H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 2nd ed., 1984.

[Bar93]

H. Barendregt. Typed lambda calculi. In Abramsky et al., editor, Handbook of Logic in Computer Science. Oxford Univ. Press, 1993.

[BBLRD96]

Z.-E.-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λυ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5), 1996.

[BG99]

R. Bloo and H. Geuvers. Explicit substitution: on the edge of strong normalization. Theoretical Computer Science, 211(1-2):375–395, 1999.

[BJO01]

F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-Data-Type Systems. Theoretical Computer Science, 277, 2001.

[BKKR01]

P. Borovanský, C. Kirchner, H. Kirchner, and C. Ringeissen. Rewriting with strategies in ELAN: a functional semantics. International Journal of Foundations of Computer Science, 12(1):69–98, February 2001.

[BKR00]

E. Bonelli, D. Kesner, and A. Ríos. A de bruijn notation for higher-order rewriting. In L. Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of LNCS, pages 62–79, Norwich, UK, July 2000. Springer-Verlag.

[Blo97]

R. Bloo. Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology, 1997.

[BN98]

F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[BR95]

R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computing Science in the Netherlands, pages 62–72. Netherlands Computer Science Research Foundation, 1995.

[CHL96]

P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, March 1996.

[Chu41]

A. Church. The Calculi of Lambda Conversion. Princeton University Press, Princeton, 1941.

[Cir00]

H. Cirstea. Calcul de réécriture : fondements et applications. PhD thesis, Université Henri Poincaré - Nancy I, 2000. October 25.

[CK98]

H. Cirstea and C. Kirchner. ρ-calculus, the rewriting calculus. In 5th International Workshop on Constraints in Computational Logics, 1998.

[CK99a]

S. Cerrito and D. Kesner. Pattern matching as cut elimination. In Longo [Lon99].

[CK99b]

H. Cirstea and C. Kirchner. Combining higher-order and first-order computation using ρ-calculus: Towards a semantics of ELAN. In D. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, Research Studies, pages 95–120. Wiley, 1999.

[CK01]

H. Cirstea and C. Kirchner. The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427–498, May 2001.

[CKL01a]

H. Cirstea, C. Kirchner, and L. Liquori. Matching Power. In A. Middeldorp, editor, 12th International Conference on Rewriting Techniques and Applications, volume 2051 of LNCS, pages 77–92, Utrecht, The Netherlands, May 2001. Springer-Verlag.

[CKL01b]

H. Cirstea, C. Kirchner, and L. Liquori. The rho cube. In F. Honsell, editor, Foundations of Software Science and Computation Structures, volume 2030 of LNCS, pages 166–180, Genova, Italy, April 2001. Springer-Verlag.

[CMMU00]

E. Contejean, C. Marché, B. Monate, and X. Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/.

[Coq00]

C. Coquand. Agda, 2000. http://www.cs.chalmers.se/~catarina/agda/.

[dB72]

N. G. de Bruijn. Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. of the Koninklijke Nederlands Akademie, 75(5):380–392, 1972.

[DG01]

R. David and B. Guillaume. A λ-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science, 11(1), 2001.

[ELA]

The ELAN system. http://elan.loria.fr/.

[Fef86]

S. Feferman, editor. Kurt Gödel, Collected Works. Oxford University Press, 1986. 2 volumes.

[FK02]

G. Faure and C. Kirchner. Exceptions in the rewriting calculus. In Tison [Tis02], pages 64–82.

[FK03]

J. Forest and D. Kesner. Expression reduction systems with patterns. In R. Nieuwenhuis, editor, 14th International Conference on Rewriting Techniques and Applications, volume 2706 of LNCS, pages 107–122, Valencia, Spain, June 2003. Springer-Verlag.

[FKP99]

M. C. Ferreira, D. Kesner, and L. Puel. Lambda-calculi with Explicit Substitutions Preserving Strong Normalization. Applicable Algebra in Engineering Communication and Computing, 9(4):333–371, 1999.

[For02a]

J. Forest. A weak calculus with explicit operators for pattern matching and substitution. In Tison [Tis02], pages 174–191.

[For02b]

J. Forest. A weak calculus with explicit operators for pattern matching and substitution. Research Report 1313, LRI, May 2002.

[Gen69]

G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen. North-Holland, 1969.

[GLM92]

G. Gonthier, J.-J. Lévy, and P.-A. Mellies. An abstract standardisation theorem. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, 1992.

[Göd31]

K. Gödel. Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931. Reprinted in [Fef86].

[Hal]

T. Hallgren. Alfa web page. http://www.cs.chalmers.se/~hallgren/Alfa/.

[Har02]

R. Harper. Programming in standard ML. Available from http://www-2.cs.cmu.edu/~rwh/smlbook/, March 2002.

[HPJP92]

P. Hudak, S. Peyton-Jones, and Philip Wadler (editors). Report on the programming language Haskell, a non-strict, purely functional language (version 1.2). Sigplan Notices, 1992.

[Isa]

The ISABELLE system. http://isabelle.in.tum.de/.

[JR99]

J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Longo [Lon99].

[Kes93]

D. Kesner. La définition de fonctions par cas à l'aide de motifs dans des langages applicatifs. Thèse de doctorat, Université Paris-Sud, Orsay, France, December 1993.

[Kha90]

Z. Khasidashvili. Expression Reduction Systems. In Proceedings of IN Vekua Institute of Applied Mathematics, volume 36, Tbilisi, 1990.

[KL91]

E. Kounalis and D. Lugiez. Compilation of pattern matching with associative commutative functions. In S. Abramsky and T. S. E. Maibaum, editors, Colloquium on Trees in Algebra and Programming, volume 493 of LNCS. Springer-Verlag, April 1991.

[Klo80]

J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127, Mathematisch Centrum, Amsterdam, 1980.

[Klo90]

J. W. Klop. Term rewriting systems. Technical report CS-R9073XS, CWI, Amsterdam, 1990.

[KPT96]

D. Kesner, L. Puel, and V. Tannen. A Typed Pattern Calculus. Information and Computation, 124(1):32–61, January 1996.

[LM92]

X. Leroy and M. Mauny. The Caml Light system, release 0.5. INRIA, Rocquencourt, 1992.

[LM01]

F. Le Fessant and L. Maranget. Optimizing pattern-matching. In Proceedings of the 2001 International Conference on Functional Programming. ACM Press, 2001.

[Lon99]

G. Longo, editor. Fourteenth Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999. IEEE Comp. Soc. Press.

[Mar92]

L. Maranget. La stratégie paresseuse. Thèse de doctorat, Université Paris 7, 1992.

[Mel95]

P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In International Conference of Typed Lambda Calculi and Applications, 1995.

[MN98]

R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, February 1998.

[New42]

M. H. A. Newman. On theories with a combinatorial definition of `equivalence'. Ann. Math., 43(2):223–243, 1942.

[Nip91]

T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.

[NM88]

G. Nadathur and D. Miller. An overview of λprolog. In Proc. 5th Int. Symp. on Logic Programming, 1988.

[Obj]

The Objective Caml language. http://www.ocaml.org/.

[Oos90]

V. V. Oostrom. Lambda calculus with patterns. Technical Report IR 228, Vrije Universiteit, Amsterdam, November 1990.

[OR93a]

V. V. Oostrom and F. V. Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, First International Workshop HOA93, volume 816 of Lecture Notes in Computer Science, Amsterdam, The Netherlands, September 1993. Springer.

[OR93b]

V. V. Oostrom and F. V. Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Research Report CS-R9361, CWI, Sep 1993.

[Par91]

M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural deduction. Author address: Equipe de Logique - CNRS UA753 45-55 5eme etage, Universite Paris VII, 2 Place Jussieu, 75251 PARIS Cedex 05 - FRANCE, E-mail: parigot@logique.jussieu.fr, 1991.

[PS93]

L. Puel and A. Suarez. Compiling pattern matching by term decomposition. Journal of Symbolic Computation, 15:1–26, 1993.

[Raa96]

F. V. Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Netherlands, 1996.

[Rit94]

E. Ritter. Normalisation for typed lambda calculi with explicit substitution. LNCS, 832:295–304, 1994.

[RS94]

J. Rehof and M. H. Sørensen. The λ_Δ calculus. In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software (TACS), number 789 in lncs, pages 516–542. Springer-Verlag, 1994.

[Sch88]

P. Schnoebelen. Refined compilation of pattern-matching for functional languages. Science of Computer Programming, 11(2):133–159, December 1988.

[Tak89]

M. Takahashi. Parallel reductions in λ-calculus. Journal of Symbolic Computation, 7(2):113–123, 1989.

[Tak93]

M. Takahashi. Parallel reductions in λ-calculus. Technical report, Department of Information Science, Tokyo Institute of Technology, 1993. Internal report.

[Tis02]

S. Tison, editor. 13th International Conference on Rewriting Techniques and Applications, volume 2378 of LNCS, Copenhagen, Denmark, July 2002. Springer-Verlag.

[Urb01]

X. Urbain. Approche incrémentale des preuves automatiques de terminaison. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 2001. http://www.lri.fr/~urbain/textes/these.ps.gz.

[Wan84]

M. Wand. What is lisp ? The American Mathematical Monthly, 91(1):32–42, January 1984.