Parsers, whether constructed by hand or automatically via a parser generator tool, typically need to compute some useful semantic information in addition to the purely syntactic analysis of their input. Semantic actions may be added to parsing code by hand, or the parser generator may have its own syntax for annotating grammar rules with semantic actions. In this paper, we take a functional programming view of such actions. We use concepts from the semantics of mostly functional programming languages and adapt them to give meaning to the actions of the parser. Specifically, the semantics is inspired by the categorical semantics of lambda calculi and the use of premonoidal categories for the semantics of effects in programming languages. This framework is then applied to our leading example, the transformation of grammars to eliminate left recursion. The syntactic transformation of left-recursion elimination leads to a corresponding semantic transformation of the actions for the grammar. We prove the semantic transformation correct and relate it to continuation passing style, a widely studied transformation in lambda calculi and functional programming.

Abstract We combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.

We define a type system, which may also be considered as a simple Hoare logic, for a fragment of an assembly language that deals with code pointers and jumps. The typing is aimed at local reasoning in the sense that only the type of a code pointer is needed, and there is no need to know the whole code itself. The main features of the type system are separation logic connectives for describing the heap, and polymorphic answer types of continuations for keeping track of jumps. Specifically, we address an interaction between separation and answer types: frame rules for local reasoning in the presence of jumps are recovered by instantiating the answer type. However, the instantiation of answer types is not sound for all types. To guarantee soundness, we restrict instantiation to closed types, where the notion of closedness arises from biorthogonality (in a sense inspired by Krivine and Pitts). A machine state is orthogonal to a disjoint heap if their combination does not lead to a fault. Closed types are sets of machine states that are orthogonal to a set of heaps. We use closed types as well-behaved answer types.

First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the source language and in the target language of the continuation-passing transform. In this paper, we establish the connection between an effect system for first-class continuations and typed versions of continuation-passing style. A region in the effect system determines a local answer type for continuations, such that the continuation transforms of pure expressions are parametrically polymorphic in their answer types. We use this polymorphism to derive transforms that make use of effect information, in particular, a mixed linear/non-linear continuation-passing transform, in which expressions without control effects are passed their continuations linearly.