Abstract effects and proof-relevant logical relations

DOI10.1145/2535838.2535869zbMath1284.68371arXiv1212.5692OpenAlexW2076954302MaRDI QIDQ5408454

Nick Benton, Martin Hofmann, Vivek Nigam

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1212.5692

zbMATH Keywords

program transformationlogical relationsparametricitytype and effect systemsregion analysis

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (7)

On the Versatility of Open Logical Relations ⋮ Counting Successes: Effects and Transformations for Non-deterministic Programs ⋮ A model of PCF in guarded type theory ⋮ Unnamed Item ⋮ Proof-Relevant Logical Relations for Name Generation ⋮ Logical Relations and Nondeterminism ⋮ Relational cost analysis in a functional-imperative setting

This page was built for publication: Abstract effects and proof-relevant logical relations