2 citations · 2 across the 2 of their papers we have counts for
3 papers
cs.LO2017
Proof-Relevant Logical Relations for Name Generation
Nick Benton, Martin Hofmann, Vivek Nigam
Pitts and Stark's -calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $ν…
cs.PL2015★ 2 cited
Effect-Dependent Transformations for Concurrent Programs
Nick Benton, Martin Hofmann, Vivek Nigam
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 number of genera…
cs.PL2012
Abstract Effects and Proof-Relevant Logical Relations
Nick Benton, Martin Hofmann, Vivek Nigam
We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant general…