A Visual Environment for Developing Context-Sensitive Term Rewriting Systems

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 R5 RS Scheme.

• Type: Conference
• Year: 2004
• Where: RTA
• Authors: Jacob Matthews, Robert Bruce Findler, Matthew Flatt, Matthias Felleisen
• Keywords: Context-sensitive Term-rewriting Semantics, Context-sensitive Term-rewriting Systems, RTA 2004, Theoretical Computer Science, Type Soundness Proofs