A Derivational Approach to the Operational Semantics of Functional Languages

Research output: Book/anthology/dissertation/reportPh.D. thesisResearch

    Malgorzata Biernacka, Denmark
  • Department of Computer Science
We study the connections between different forms of operational semantics for functional programming languages and we present systematic methods of interderiving reduction semantics, abstract machines and higher-order evaluators. We first consider two methods based on program transformations: a syntactic correspondence relating reduction semantics and abstract machines, and a functional correspondence relating abstract machines and higher-order evaluators. We show that an extension of the syntactic correspondence provides a systematic and uniform derivation method connecting calculi of explicit substitutions and environment machines. In particular, we show that canonical environment-based abstract machines for evaluation in the lambda calculus, including the Krivine machine for call by name and the CEK machine for call by value, can be systematically derived from a calculus of explicit substitutions, given a reduction strategy such as normal order or applicative order. Furthermore, we show that the syntactic correspondence applies to languages with context-sensitive reductions, which we illustrate by presenting a number of calculi of explicit substitutions with computational effects (e.g., control operators, input/output, stack inspection, laziness and proper tail recursion). Several of the corresponding abstract machines have been independently designed and reported as such in the literature. All the calculi are new. As an application of the syntactic and the functional correspondences, we also provide an operational foundation for the lambda calculus with a hierarchy of delimited control operators, shift and reset. In addition, we present a case study in program extraction from proofs, using Kreisel’s modified realizability. This case study provides another example of a derivational approach to connecting semantic specifications: we formalize the reduction semantics of the simply typed lambda calculus in a first-order logic, and from the proof of weak head normalization we extract a higher-order evaluator for this language.
Original languageEnglish
Place of publicationAarhus
Number of pages195
Publication statusPublished - 2006
SeriesDaimi PhD Dissertation

See relations at Aarhus University Citationformats

ID: 3782511