Martin Churchill
My interests center around programming language semantics. I have previously worked in semantics for a quantum language, game semantics, and a modular semantics framework.
Research Areas
Authored Publications
Google Publications
Other Publications
Sort By
Reusable Components of Semantic Specifications
Peter D. Mosses
Neil Sculthorpe
Paolo Torrini
Lecture Notes in Computer Science, vol. 8989 (2015), pp. 132-179
Preview abstract
Semantic specifications of programming languages typically have poor modularity. This hinders reuse of parts of the semantics of one language when specifying a different language – even when the two languages have many constructs in common – and evolution of a language may require major reformulation of its semantics. Such drawbacks have discouraged language developers from using formal semantics to document their designs.
In the PLanCompS project, we have developed a component-based approach to semantics. Here, we explain its modularity aspects, and present an illustrative case study: a component-based semantics for Caml Light. We have tested the correctness of the semantics by running programs on an interpreter generated from the semantics, comparing the output with that produced on the standard implementation of the language.
Our approach provides good modularity, facilitates reuse, and should support co-evolution of languages and their formal semantics. It could be particularly useful in connection with domain-specific languages and language-driven software development.
View details
Imperative programs as proofs via game semantics
Imperative Programs as Proofs via Game Semantics
Modular Semantics for Transition System Specifications with Negative Premises
Modular Bisimulation Theory for Computations and Values
Imperative Programs as Proofs via Game Semantics
A Concrete Representation of Observational Equivalence for PCF
A Logic of Sequentiality
