TermWare3 – term rewriting system, based on context-term calculus

R.S. Shevchenko, A.Yu. Doroshenko


In this paper, the design of the TermWare-3 rewriting system which is built on the ground of reflective calculus of context term is considered. In the calculus of the context term, term structure contains not only tree, but a reference to an internal context and matching constrains (external context). This allows to embed operation of name resolving into the mathematical semantics of the term rewriting.  The elements of algebra are multiterms, which complement context terms by constructions of arrows, universal matching pattern and consistent set. This allows to emulate substitutions of typed variables in the terms of multiterm algebra. Also, the method of effective rule dispatch is described. Example of usage term re­writing system for checking of smart-contract properties, with automatic transformation of expression between representation in terms of Scala algebraic types and TermWare-3 context terms
is shown. 

Problems in programming 2019; 1: 48-58


automated software design; programming languages; term rewriting; type systems; code analysis; TermWare

Full Text:

PDF (Ukrainian)


Shevchenko R., Doroshenko A. Managing Business Logic with Symbolic Computation. Information Systems Technology and Applications: Proc. 2-nd Intern. Conf. ISTA'2003, June 19–21, 2003. Kharkiv, Ukraine. P. 143–152.

Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003.

Doroshenko A., Shevchenko R. A rewriting framework for rule-based programming dynamic applications. Fundamenta Infor-maticae. 2006. Vol. 72, N 1–3. P. 95–108.

Eugene Tulika, Anatoliy Doroshenko, Kostiantyn Zhereb. Using Choreography of Actors and Rewriting Rules to Adapt Lega-cy Fortran Programs to Cloud Computing. June 2017. Communications in Computer and Information Science.

Ethereum Foundation. The solidity contract-oriented programming language.

Jeremy Gibbons and Nicolas Wu. Folding domain-specific languages: deep and shallow embeddings (functional Pearl). In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (ICFP '14). 2014. ACM, New York, NY, USA.


Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS'16). ACM, New York, NY, USA. P. 254–269. CrossRef

"Report of Investigation Pursuant to Section 21(a) of the Securities Exchange Act of 1934: The DAO" (PDF). Securities and Exchange Commission. July 25, 2017.



  • There are currently no refbacks.