Ptolemy: A Language of Quantified, Typed Events

This paper defines Ptolemy. The novelty of Ptolemy is the notion of event types and quantification based on event types. We give the syntax, operational semantics and type rules for the langauge, and discuss its meta-theory. 1. Ptolemy’s Design In this section, we describe Ptolemy, a language with quantified, typed events that extends implicit invocation (II) languages with ideas from aspect-oriented (AO) languages. Ptolemy features new mechanisms for declaring event types and events. Our description includes syntax, examples, semantics, and type checking rules. 1.1 Overview Ptolemy is inspired by II languages such as Rapide [8] and AO lan-guages such as AspectJ [5]. It also incorporates some ideas from Eos [11] and Caesar [9]. As a small, core language, its techni