Expression Reduction Systems and Extensions: An Overview | SpringerLink
Skip to main content
Springer Nature Link
Log in

Expression Reduction Systems and Extensions: An Overview

  • Chapter
Processes, Terms and Cycles: Steps on the Road to Infinity

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3838))

  • 517 Accesses

Abstract

Expression Reduction Systems is a formalism for higher-order rewriting, extending Term Rewriting Systems and the lambda-calculus. Here we give an overview of results in the literature concerning ERSs. We review confluence, normalization and perpetuality results for orthogonal ERSs. Some of these results are extended to orthogonal conditional ERSs. Further, ERSs with patterns are introduced and their confluence is discussed. Finally, higher-order rewriting is translated into equational first-order rewriting. The technique develops an isomorphic model of ERSs with variable names, based on de Bruijn indices.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 4(1), 375–416 (1991)

    Article  Google Scholar 

  2. The Alfa proof editor, http://www.cs.chalmers.se/~hallgren/Alfa/

  3. Ariola, Z., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Proceedings of the 22nd Symposium on Principles of Programming Languages, pp. 233–246. ACM Press, New York (1995)

    Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  5. Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984) (Revised Edition)

    MATH  Google Scholar 

  6. Barendregt, H., Bergstra, J.A., Klop, J.-W., Volken, H.: Some notes on lambda-reduction in “degrees, reductions, and representability in the lambda calculus”. Technical Report 22, Department of mathematics, University of Utrecht (1976)

    Google Scholar 

  7. Barendregt, H., Kennaway, R., Klop, J.-W., Sleep, M.R.: Needed reduction and spine strategies for the lambda calculus. Information and Computation 75(3), 191–231 (1987)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  9. Bergstra, J.A., Klop, J.-W.: Strong normalization and perpetual reductions in the lambda calculus. Journal of Information Processing and Cybernetics 18(7/8), 403–417 (1982)

    MATH  MathSciNet  Google Scholar 

  10. Bergstra, J.A., Klop, J.-W.: Conditional rewrite rules: confluence and termination. Journal of Computer and System Science 32(3), 323–362 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  11. Bloo, R., Rose, K.: Combinatory reduction systems with explicit substitution that preserve strong normalisation. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 169–183. Springer, Heidelberg (1996)

    Google Scholar 

  12. Bonelli, E.: A normalization result for higher-order calculi with explicit substitutions. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 153–168. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Bonelli, E., Kesner, D., Ríos, A.: De Bruijn indices for metaterms. Journal of Logic and Computation (to appear)

    Google Scholar 

  14. Bonelli, E., Kesner, D., Ríos, A.: Relating higher-order and first-order rewriting. Journal of Logic and Computatio (to appear)

    Google Scholar 

  15. Bonelli, E., Kesner, D., Ríos, A.: A de Bruijn notation for higher-order rewriting. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 62–79. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Bonelli, E., Kesner, D., Ríos, A.: From higher-order to first-order rewriting (extended abstract). In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 47–62. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Boudol, G.: Computational semantics of term rewriting systems. In: Nivat, M., Reynolds, J. (eds.) Algebraic methods in semantics, pp. 169–236. Cambridge University Press, Cambridge (1985)

    Google Scholar 

  18. Bourbaki, N.: Elements of Mathematics, Theory of Sets. Addison-Wesley, Reading (1968)

    MATH  Google Scholar 

  19. Briaud, D.: An explicit eta rewrite rule. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 94–108. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  20. Burstall, R., MacQueen, D., Sanella, D.: Hope: An experimental applicative language. In: Proceedings of the LISP Conference, pp. 136–143. Stanford University, Computer Science Department (1980)

    Google Scholar 

  21. Cerrito, S., Kesner, D.: Pattern matching as cut elimination. In: 14th Symposium on Logic in Computer Science, pp. 98–108. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  22. Cerrito, S., Kesner, D.: Pattern matching as cut elimination. Theoretical Computer Science 323, 71–127 (2004)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  24. The Coq Proof Assistant, http://coq.inria.fr/

  25. Curien, P.-L.: Categorical combinators, sequential algorithms and functional programming, 1st edn. Progress in Theoretical Computer Science. Birkhäuser, Basel (1986)

    MATH  Google Scholar 

  26. Curien, P.-L.: Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report 1617, INRIA-Rocquencourt (1992)

    Google Scholar 

  27. de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Mathematicae 5(35), 381–392 (1972)

    Article  Google Scholar 

  28. de Bruijn., N.G.: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report 78-WSK-03, Eindhoven University of Technology (1978)

    Google Scholar 

  29. Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 538–549. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  30. Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: 10th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1995)

    Google Scholar 

  31. Dowek, G., Hardin, T., Kirchner, C.: Unification via explicit substitutions: The case of higher-order patterns. Technical Report RR3591, INRIA (1998)

    Google Scholar 

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

  33. Forest, J.: A weak calculus with explicit operators for pattern matching and substitution. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 174–191. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  34. Forest, J., Kesnerp, D.: Expression reduction systems with patterns. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 107–122. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  35. Glauert, J., Kennaway, R., Khasidashvili, Z.: Stable results and relative normalization. Journal of Logic and Computation 10(3), 323–348 (2000); Special Issue: Type Theory and Term Rewriting

    Article  MATH  MathSciNet  Google Scholar 

  36. Glauert, J., Khasidashvili, Z.: An abstract Böhm-normalization. In: 2nd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol. 70(6). Elsevier Science, Amsterdam (2002)

    Google Scholar 

  37. Gramlich, B.: Termination and confluence properties of structured rewrite systems. PhD thesis, Universität Kaiserslautern, Germany (1996)

    Google Scholar 

  38. Hanus, M., Prehofer, C.: Higher-order narrowing with definitional trees. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 138–152. Springer, Heidelberg (1996)

    Google Scholar 

  39. Hardin, T.: η-reduction for explicit substitutions. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 306–321. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  40. Hardin, T., Lévy, J.-J.: A confluent calculus of substitutions. In: France-Japan Artificial Intelligence and Computer Science Symposium, Izu, Japan (1989)

    Google Scholar 

  41. Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambda-sigma calculus. In: Proceedings of the International Conference on Functional Programming, pp. 25–33. ACM Press, New York (1996)

    Google Scholar 

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

    Google Scholar 

  43. Huet, G., Lévy, J.-J.: Computations in orthogonal rewriting systems. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 394–443. MIT Press, Cambridge (1991)

    Google Scholar 

  44. The Isabelle theorem prover, http://isabelle.in.tum.de/

  45. Barry Jay, C.: The pattern calculus. ACM Transactions on Programming Languages and Systems 26(6), 911–937 (2004)

    Article  Google Scholar 

  46. Jouannaud, J.-P., Okada, M.: A computation model for executable higher-order algebraic specification languages. In: 6th Symposium on Logic in Computer Science, pp. 350–361. IEEE Computer Society Press, Los Alamitos (1991)

    Chapter  Google Scholar 

  47. Kamareddine, F., Ríos, A.: A λ-calculus à la de Bruijn with explicit substitutions. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, pp. 45–62. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  48. Kesner, D.: Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 184–199. Springer, Heidelberg (1996)

    Google Scholar 

  49. Kesner, D.: Confluence of extensional and non-extensional lambda-calculi with explicit substitutions. Theoretical Computer Science 238(1-2), 183–220 (2000)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  51. Khasidashvili, Z.: β-reductions and β-developments of λ-terms with the least number of steps. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 105–111. Springer, Heidelberg (1990)

    Google Scholar 

  52. Khasidashvili, Z.: Expression reduction systems. Technical Report 36: 200-220, I. Vekua Institute of Applied Mathematics of Tbilisi State University (1990)

    Google Scholar 

  53. Khasidashvili, Z.: The church-rosser theorem in orthogonal combinatory reduction systems. Technical Report 1825, INRIA-Rocquencourt (1992)

    Google Scholar 

  54. Khasidashvili, Z.: The longest perpetual reductions in orthogonal expression reduction systems. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 191–203. Springer, Heidelberg (1994)

    Google Scholar 

  55. Khasidashvili, Z.: On higher order recursive program schemes. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 172–186. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  56. Khasidashvili, Z.: Perpetuality and strong normalization in orthogonal term rewriting systems. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol. 775, pp. 163–174. Springer, Heidelberg (1994)

    Google Scholar 

  57. Khasidashvili, Z.: On the longest perpetual reductions in orthogonal expression reduction systems. Theoretical Computer Science 266(1/2), 737–772 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  58. Khasidashvili, Z.: Optimal normalization in orthogonal term rewriting systems. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 243–258. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  59. Khasidashvili, Z., Glauert, J.: Relating conflict-free stable transition and event models via redex families. Theoretical Computer Science 286(1), 65–95 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  60. Khasidashvili, Z., Glauert, J.: An abstract concept of optimal implementation. In: 3rd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol. 84(4). Elsevier Science, Amsterdam (2003)

    Google Scholar 

  61. Khasidashvili, Z., Glauert, J.: Stable computational semantics of conflict-free rewrite systems (partial orders with erasure). In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 467–482. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  62. Khasidashvili, Z., Glauert, J.: The geometry of conflict-free reduction spaces. Theoretical Computer Science (2005) (to appear)

    Google Scholar 

  63. Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Perpetuality and uniform normalization in orthogonal rewrite systems. Information and Computation 164(1), 118–151 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  64. Khasidashvili, Z., Piperno, A.: Perpetuality and uniform normalization. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP 1997 and HOA 1997. LNCS, vol. 1298, pp. 240–255. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  65. Khasidashvili, Z., van Oostrom, V.: Context-sensitive conditional expression reduction systems. In: Workshop on Graph Rewriting and Computation. Electronic Notes in Theoretical Computer Science, vol. 2. Elsevier Science, Amsterdam (1995)

    Google Scholar 

  66. Khasidashvili, Z., van Oostrom, V.: Context-sensitive conditional rewrite systems. Technical Report SYS–C95–06, University of East Anglia (1995)

    Google Scholar 

  67. Klop, J.-W.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam (1980)

    Google Scholar 

  68. Klop, J.-W.: Term Rewriting Systems. Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Oxford University Press, Oxford (1992)

    Google Scholar 

  69. Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121(1/2), 279–308 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  70. Lévy, J.-J.: Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université Paris VII, France (1978)

    Google Scholar 

  71. Lévy, J.-J.: Optimal reductions in the lambda-calculus. In: Hindley, J.R., Seldin, J.P., Curry, T.H.B. (eds.), pp. 159–192. Academic Press, London (1980)

    Google Scholar 

  72. Maranget, L.: Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. In: Proceedings of the 18th Symposium on Principles of Programming Languages, pp. 255–269. ACM Press, New York (1991)

    Google Scholar 

  73. The MAUDE System, http://maude.cs.uiuc.edu/

  74. Melliès, P.-A.: Description Abstraite des Systèmes de Réécriture. PhD thesis, Université Paris VII (1996)

    Google Scholar 

  75. Melliès, P.-A.: Axiomatic rewriting theory II: the lambda-sigma calculus enjoys finite normalisation cones. Journal of Logic and Computation 10(3), 461–487 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  76. Middeldorp, A.: Call by need computations to root-stable form. In: Proceedings of the 24th Symposium on Principles of Programming Languages, pp. 94–105. ACM Press, New York (1997)

    Google Scholar 

  77. Milner, R.: Functions as processes. Mathematical Structures in Computer Science 2(2), 119–141 (2005)

    Article  MathSciNet  Google Scholar 

  78. Milner, R., Tofte, M., Harper, R.: The definition of Standard ML. MIT Press, Cambridge (1990)

    Google Scholar 

  79. Muñoz, C.: A left-linear variant of λσ. In: Join International Conference on Algebraic and Logic Programming and International Workshop on Higher-Order Algebra. LNCS, vol. 1298, pp. 224–239. Springer, Heidelberg (1997)

    Google Scholar 

  80. Nederpelt, R.: Strong normalization for a typed lambda-calculus with lambda structured types. PhD thesis, Technische Hogeschool Eindhoven, Netherlands (1973)

    Google Scholar 

  81. Nipkow, T.: Higher-order critical pairs. In: 6th Symposium on Logic in Computer Science, pp. 342–349. IEEE Computer Society Press, Los Alamitos (1991)

    Chapter  Google Scholar 

  82. Nipkow, T.: Orthogonal higher-order rewrite systems are confluent. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 306–317. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  83. Nöcker, E.: Efficient Functional Programming: Compilation and Programming Techniques. PhD thesis, University of Nijmegen, Netherlands (1994)

    Google Scholar 

  84. The Objective Caml language, http://caml.inria.fr/

  85. O’Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol. 58. Springer, Heidelberg (1977)

    MATH  Google Scholar 

  86. Pkhakadze, S.: Some problems of the notation theory. I. Vekua Institute of Applied Mathematics of Tbilisi State University (1977) (in Russian)

    Google Scholar 

  87. Pkhakadze, S.: An n. bourbaki-type general theory and the properties of contracting symbols and corresponding contracted forms. Georgian Mathematical Journal 6(2), 179–190 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  88. Plaisted, D.: Polynomial time termination and constraint satisfaction tests. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 405–420. Springer, Heidelberg (2003)

    Google Scholar 

  89. The PVS system, http://pvs.csl.sri.com/

  90. Ríos, A.: Contribution à l’étude des λ-calculs avec substitutions explicites. Thèse de doctorat, Université de Paris VII (1993)

    Google Scholar 

  91. Rose, K.: Explicit cyclic substitutions. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 36–50. Springer, Heidelberg (1993)

    Google Scholar 

  92. Sørensen, M.H.: Normalization in λ-calculus and type theory. PhD thesis, University of Copenhagen, Denmark (1997)

    Google Scholar 

  93. Sørensen, M.H.: Properties of infinite reduction paths in untyped λ-calculus. In: 1st Tbilisi Symposium on Logic, Language and Computation, Selected papers, pp. 353–367. SiLLI Publications, CSLI, Stanford (1998)

    Google Scholar 

  94. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  95. Toyama, Y.: Confluent term rewriting systems with membership conditions. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 128–141. Springer, Heidelberg (1988)

    Google Scholar 

  96. Turner, D.: Miranda: A non-strict functional language with polymorphic types. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 1–16. Springer, Heidelberg (1985)

    Google Scholar 

  97. van Oostrom, V.: Confluence for Abstract and Higher-order Rewriting. PhD thesis, Vrije University, Amsterdam, Netherlands (1994)

    Google Scholar 

  98. van Oostrom, V., van Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 379–392. Springer, Heidelberg (1994)

    Google Scholar 

  99. van Raamsdonk, F.: Confluence and superdevelopments. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 168–182. Springer, Heidelberg (1993)

    Google Scholar 

  100. van Raamsdonk, F., Severi, P., Sørensen, M.H., Xi, H.: Perpetual reductions in λ-calculus. Information and Computation 149(2), 173–229 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  101. Wolfram, D.: The Causal Theory of Types. Cambridge Tracts in Theoretical Computer Science, vol. 21. Cambridge University Press, Cambridge (1993)

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Sciences, University of East Anglia, Norwich, UK

    John Glauert

  2. PPS, CNRS and Université Paris 7, France

    Delia Kesner

  3. Logic and Validation Technology, Design Technology Division Intel Development Center, Haifa, Israel

    Zurab Khasidashvili

Authors
  1. John Glauert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Delia Kesner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zurab Khasidashvili
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Aart Middeldorp

  2. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    Vincent van Oostrom

  3. Department of Theoretical Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081 HV, Amsterdam, The Netherlands

    Femke van Raamsdonk

  4. VU Vrije Universiteit Amsterdam,  

    Roel de Vrijer

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Glauert, J., Kesner, D., Khasidashvili, Z. (2005). Expression Reduction Systems and Extensions: An Overview. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_22

Download citation

  • DOI: https://doi.org/10.1007/11601548_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30911-6

  • Online ISBN: 978-3-540-32425-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation