Abstract
Over the past decade, researchers have found context-sensitive term-rewriting semantics to be powerful and expressive tools for modeling programming languages, particularly in establishing type soundness proofs. Unfortunately, developing such semantics is an error-prone activity. To address that problem, we have designed PLT Redex, an embedded domain-specific language that helps users interactively create and debug context-sensitive term-rewriting systems. We introduce the tool with a series of examples and discuss our experience using it in courses and developing an operational semantics for R5RS Scheme.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 235–271 (1992)
Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation (1994) 38–94 First appeared as Technical Report TR160, Rice University (1991)
Xiao, Y., Sabry, A., Ariola, Z.M.: From syntactic theories to interpreters: Automating the proof of unique decomposition. Higher-Order and Symbolic Computation 4, 387–409 (1999)
Flatt, M.: PLT MzScheme: Language manual. Technical Report TR97-280, Rice University (1997), http://www.mzscheme.org/
Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)
Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics. Studies in Logics and the Foundations of Mathematics, vol. 103. North Holland, Amsterdam (1981)
Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer’s reduction semantics for classes and mixins. Formal Syntax and Semantics of Java 1523, 241–269 (1999); Preliminary version appeared in proceedings of Principles of Programming Languages (1998); Revised version is Rice University technical report TR 97-293 (June 1999)
Kelsey, R., Clinger, W., J.R.: Revised5 report of the algorithmic language Scheme. ACM SIGPLAN Notices, 33, 26–76 (1998)
Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.E., Vittek, M.: ELAN: A logical framework based on computational systems. In: Proc. of the First Int. Workshop on Rewriting Logic, vol. 4, Elsevier, Amsterdam (1996)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001)
Visser, E.: Stratego: A language for program transformation based on rewriting strategies. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001)
van den Brand, M.G.J., Heering, J., Klint, P., Oliver, P.A.: Compiling language definitions: The ASF+SDF compiler. ACM Transactions on Programming Languages and Systems 24, 334–368 (2002)
Lippi, S.: in2: A Graphical Interpreter for Interaction Nets (system description). In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 380–384. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matthews, J., Findler, R.B., Flatt, M., Felleisen, M. (2004). A Visual Environment for Developing Context-Sensitive Term Rewriting Systems. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive