iRho: an imperative rewriting calculus

ABSTRACT

We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-matching, pattern-abstraction, and side-effects, which we call iRho.We formulate a static and a call-by-value dynamic semantics of iRho like that of Gilles Kahn's Natural Semantics. The operational semantics is deterministic, and immediately suggests how to build an interpreter for the calculus. The static semantics is given via a first-order type system based on a form of product-type, which can be assigned to iRho-terms like structures (i.e. pairs).The calculus is à la Church, i.e. pattern-abstractions are decorated with the types of the free variables of the pattern.iRho is a good candidate for a core or an intermediate language, because it can safely access and modify a (monomorphic) typed store, and because fixed-points can be defined.Properties like determinism of the interpreter, and subject reduction are completely checked by a machine assisted approach, using the Coq proof assistant. Progress and decidability of type-checking are proved by pen and paper.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: Gilles Barthe , Horatiu Cirstea , Claude Kirchner , Luigi Liquori, Pure patterns type systems, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 15-17, 2003, New Orleans, Louisiana, USA
• 3: Gérard Boudol, The recursive record semantics of objects revisited, Journal of Functional Programming, v.14 n.3, p.263-315, May 2004 [doi>10.1017/S0956796803004775]
• 4: G. Boudol and P. Zimmer. Recursion in the Call-by-Value Lambda-Calculus. In Proc. of FICS, Note Series NS-02-2. BRICS, 2002.
• 5: 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, 2001.
• 6: Horatiu Cirstea , Claude Kirchner , Luigi Liquori, Matching Power, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.77-92, May 22-24, 2001
• 7: Horatiu Cirstea , Claude Kirchner , Luigi Liquori, The Rho Cube, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.168-183, April 02-06, 2001
• 8: H. Cirstea, C. Kirchner, and L. Liquori. Rewriting Calculus with(out) Types. In Proc. of WRLA, ENTCS, 2002.
• 9: H. Cirstea, L. Liquori, and B. Wack. Rho-calculus with Fixpoint: First-order system. In Proc. of TYPES. Springer-Verlag, 2004.
• 10: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• 11: Cristal, Foc-CNAM, Lemme, Mimosa, Miró, and Oasis. Concert: Compilateurs Certifiés, 2004. ARC INRIA 2003-2004, http://www-sop.inria.fr/lemme/concert.
• 12: G. Faure and P. Moreau. Jrho: a Java Implementation of the Rho Calculus, 2002. http://elan.loria.fr/Soft/jrho-0.1.tar.gz.
• 13: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 14: Eduardo Giménez, Structural Recursive Definitions in Type Theory, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.397-408, July 13-17, 1998
• 15: J. Goguen. The OBJ Family Home Page, 2004. http://www.cs.ucsd.edu/users/goguen/sys/obj.html.
• 16: Tom Hirschowitz , Xavier Leroy , J. B. Wells, Compilation of extended recursion in call-by-value functional languages, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.160-171, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888267]
• 17: G. Huet. Résolution d'equations dans les langages d'ordre 1,2, ...,ω. Ph.d. thesis, Université de Paris 7 (France), 1976.
• 18: Gilles Kahn, Natural Semantics, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, p.22-39, February 19-21, 1987
• 19: S. Kamin, Inheritance in smalltalk-80: a denotational definition, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-87, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73567]
• 20: P. J. Landin. The Mechanical Evaluation of Expression. The Computer Journal, 6:308--320, 1964.
• 21: Keunwoo Lee , Anthony LaMarca , Craig Chambers, HydroJ: object-oriented pattern matching for evolvable distributed systems, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 22: L. Liquori and B. Serpette. The Full Version of this paper, 2004. http://www-sop.inria.fr/oasis/Bernard.Serpette/ImpRhoCalculus/.
• 23: I. A. Mason and C. L. Talcott. References, Local Variables and Operational Reasoning. In Proc. of LICS, pages 66--77, 1992.
• 24: Paul Francis Mendler, Inductive definition in type theory, 1988
• 25: N. P. Mendler, P. Panangaden, and R. L. Constable. Infinite Objects in Type Theory. In Proc. of LICS, pages 249--255, 1986.
• 26: Microsoft. The C# Home Page, 2004. http://msdn.microsoft.com/vcsharp/.
• 27: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 28: P. Moreau, C. Ringeissen, and M. Vittek. The Tom Home Page, 2004. http://tom.loria.fr/.
• 29: Greg Morrisett , Matthias Felleisen , Robert Harper, Abstract models of memory management, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.66-77, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224182]
• 30: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 31: Dirk Riehle , Heinz Züllighoven, Understanding and using patterns in software development, Theory and Practice of Object Systems, v.2 n.1, p.3-13, 1996 [doi>10.1002/(SICI)1096-9942(1996)2:1<3::AID-TAPO1>3.0.CO;2-#]
• 32: A. Stump. The Rogue Home Page, 2004. http://www.cse.wustl.edu/~stump/rogue.html.
• 33: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 34: Sun. Java Technology, 2004. http://java.sun.com/.
• 35: The Asf+Sdf Team. The Asf+Sdf Meta-Environment Home Page, 2004. http://www.cwi.nl/htbin/sen1/twiki/bin/view/SEN1/MetaEnvironment.
• 36: The Cduce Team. The Cduce Home Page, 2004. http://www.cduce.org.
• 37: The Common Criteria Consortium. The Common Criteria Home Page, 2004. http://www.commoncriteria.org.
• 38: The Cristal Team. The Objective Caml Home Page, 2004. http://www.ocaml.org/.
• 39: The GNU Prolog Team. The GNU Prolog Home Page, 2004. http://pauillac.inria.fr/~diaz/gnu-prolog/.
• 40: The Haskell Team. The Haskell Home Page, 2004. http://www.haskell.org/.
• 41: The Logical Team. The Coq Home Page, 2004. http://coq.inria.fr.
• 42: The Maude Team. The Maude Home Page, 2004. http://maude.cs.uiuc.edu/.
• 43: The Mimosa Team. The Schme Bigloo Home Page, 2004. http://www.sop.inria.fr/mimosa/fp/bigloo/.
• 44: The Protheo Team. The Elan Home Page, 2004. http://elan.loria.fr.
• 45: The Scheme Team. The Scheme Language, 2004. http://www.swiss.ai.mit.edu/projects/scheme/.
• 46: The Stratego Team. The Rho Stratego Home Page, 2004. http://www.stratego-language.org/twiki/bin/view/Stratego/RhoStratego.
• 47: The Stratego Team. The Stratego Home Page, 2004. http://www.stratego-language.org.
• 48: The Xduce Team. The Xduce Home Page, 2004. http://xduce.sourceforge.net.
• 49: A. van Deursen, J. Heering, and P. Klint. Language Prototyping. World Scientific, 1996.
• 50: V. van Oostrom. Lambda Calculus with Patterns. Technical Report IR-228, Faculteit der Wiskunde en Informatica, Vrije Universiteit Amsterdam, 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages; Applicative (functional) languages

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving; Lambda calculus and related systems; Logic and constraint programming

General Terms:
Languages, Theory

Keywords:
certied software, natural semantics, pattern-matching, rewriting-calculus, term rewriting systems, types