@article{benton18scp, author = {Benton, Nick and Hofmann, Martin and Nigam, Vivek}, title = {Effect-dependent transformations for concurrent programs}, journal = {Sci. Comput. Program.}, volume = {155}, pages = {27--51}, year = {2018}, abstract = {We describe a denotational semantics for an abstract effect system for a higher-order,shared-variable concurrent programming language. We prove the soundness of a numberof general effect-based program equivalences, including a parallelization equationthat specifies sufficient conditions for replacing sequential composition with parallelcomposition. Effect annotations are relative to abstract locations specified by contractsrather than physical footprints allowing us in particular to show the soundness of sometransformations involving fine-grained concurrent data structures, such as MichaelScottqueues, that allow concurrent access to different parts of mutable data structures.Our semantics is based on refining a trace-based semantics for first-order programsdue to Brookes. By moving from concrete to abstract locations, and adding type refinementsthat capture the possible side-effects of both expressions and their concurrentenvironments, we are able to validate many equivalences that do not hold in an unrefinedmodel. The meanings of types are expressed using a game-based logical relationover sets of traces. Two programs e1 and e2 are logically related if one is able to solvea two-player game: for any trace with result value v1 in the semantics of e1 (challenge)that the player presents, the opponent can present an (response) equivalent trace in thesemantics of e2 with a logically related result value v2.}, doi = {10.1016/j.scico.2017.11.001}, url = {https://doi.org/10.1016/j.scico.2017.11.001}, } @article{benton18lmcs, author = {Benton, Nick and Hofmann, Martin and Nigam, Vivek}, title = {Proof-Relevant Logical Relations for Name Generation}, journal = {Accepted to Logical Methods in Computer Science}, year = {2018}, abstract = {Pitts and Stark’s v-calculus is a paradigmatic total language for studying the problem ofcontextual equivalence in higher-order languages with name generation. Models for the ν-calculusthat validate basic equivalences concerning names may be constructed using functor categories ornominal sets, with a dynamic allocation monad used to model computations that may allocate freshnames. If recursion is added to the language and one attempts to adapt the models from (nominal)sets to (nominal) domains, however, the direct-style construction of the allocation monad no longerworks. This issue has previously been addressed by using a monad that combines dynamic allocationwith continuations, at some cost to abstraction.This paper presents a direct-style model of a v-calculus-like language with recursion using thenovel framework of proof-relevant logical relations, in which logical relations also contain objects(or proofs) demonstrating the equivalence of (the semantic counterparts of) programs. Apart fromproviding a fresh solution to an old problem, this work provides an accessible setting in which tointroduce the use of proof-relevant logical relations, free of the additional complexities associatedwith their use for more sophisticated languages.}, }