A Weak Calculus with Explicit Operators for Pattern Matching and Substitution

1. Martín Abadi, Luca Cardelli, Pierre Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 4(1):375–416, 1991.

   Google Scholar 

2. Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne, and Jocelyne Rouyer-Degli. λυ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5):699–722, 1996.

   Article  MATH  MathSciNet  Google Scholar 

3. Roel Bloo. Preservation of strong normalization for explicit substitutions. Technical Report TR95-08, TUE Computing Science Reports, Eindhoven University of Technology, 1995.

   Google Scholar 

4. Roel Bloo and Kristoffer 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.

   Google Scholar 

5. Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, March 1996.

   Google Scholar 

6. Serenella Cerrito and Delia Kesner. Pattern matching as cut elimination, ftp://ftp.lri.fr/LRI/articles/kesner/pm-as-ce.ps.gz.

7. Horatiu Cirstea and Claude Kirchner. ρ-calculus, the rewriting calculus. In Fifth International Workshop on Constraints in Computational Logics, 1998.

   Google Scholar 

8. Serenella Cerrito and Delia Kesner. Pattern matching as cut elimination. In Giuseppe Longo, editor, Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 98–108. IEEE Computer Society Press, July 1999.

   Google Scholar 

9. Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. Matching Power. In Aart Middeldorp, editor, Proceedings ofRTA’ 2001, Lecture Notes in Computer Science, Utrecht (The Netherlands), May 2001. Springer-Verlag.

   Google Scholar 

10. René David and Bruno Guillaume. A λ-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science, 11, 2001.

    Google Scholar 

11. Maria C.F. Ferreira, Delia Kesner, and Laurence Puel. Lambda-calculi with explicit substitutions preserving strong normalization. Applicable Algebra in Engineering Communication and Computing, 9(4):333–371, 1999.

    Article  MATH  MathSciNet  Google Scholar 

12. Julien Forest. A calculus of pattern matching and explicit substitution draft. Technical Report LRI-1313, 2002. http://www.lri.fr/~forest/lpw.ps.gz.

13. Delia Kesner. Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions. In Harald Ganzinger, editor, Seventh International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 184–199. Springer-Verlag, July 1996.

    Google Scholar 

14. Jan-Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980. PhD Thesis.

    MATH  Google Scholar 

15. Delia Kesner, Laurence Puel, and Val Tannen. A Typed Pattern Calculus. Information and Computation, 124(1):32–61, 1996.

    Article  MATH  MathSciNet  Google Scholar 

16. Pierre Lescanne. From λσ to λυ, ajourney through calculi of explicit substitutions. In Annual ACM Symposium on Principles of Programming Languages (POPL), pages 60–69, Portland, Oregon, 1994.

    Google Scholar 

17. The Objective Caml language. http://caml.inria.fr/.

18. E. Ritter. Normalisation for typed lambda calculi with explicit substitution. Lecture Notes in Computer Science, 832:295–--, 1994.

    Google Scholar 

Download references