A semantics for context-sensitive reduction semantics

Casey Klein*, Jay McCarthy, Steven Jaconette, Robert Findler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations


This paper explores the semantics of the meta-notation used in the style of operational semantics introduced by Felleisen and Hieb. Specifically, it defines a formal system that gives precise meanings to the notions of contexts, decomposition, and plugging (recomposition) left implicit in most expositions. This semantics is not naturally algorithmic, so the paper also provides an algorithm and proves a correspondence with the declarative definition. The motivation for this investigation is PLT Redex, a domain-specific programming language designed to support Felleisen-Hieb-style semantics. This style of semantics is the de-facto standard in operational semantics and, as such, is widely used. Accordingly, our goal is that Redex programs should, as much as possible, look and behave like those semantics. Since Redex's first public release more than seven years ago, its precise interpretation of contexts has changed several times, as we repeatedly encountered reduction systems that did not behave according to their authors' intent. This paper describes the culimation of that experience. To the best of our knowledge, the semantics given here accommodates even the most complex uses of contexts available.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 9th Asian Symposium, APLAS 2011, Proceedings
Number of pages15
StatePublished - 2011
Event9th Asian Symposium on Programming Languages and Systems, APLAS 2011 - Kenting, Taiwan, Province of China
Duration: Dec 5 2011Dec 7 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7078 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th Asian Symposium on Programming Languages and Systems, APLAS 2011
Country/TerritoryTaiwan, Province of China

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A semantics for context-sensitive reduction semantics'. Together they form a unique fingerprint.

Cite this