More Web Proxy on the site http://driver.im/

research-article

Abstract effects and proof-relevant logical relations

Authors:

Martin Hofmann,

Vivek NigamAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 1

Pages 619 - 631

https://doi.org/10.1145/2578855.2535869

Published: 08 January 2014 Publication History

Abstract

We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as 'pure' or 'read only'. This 'fictional purity' allows clients of a module to validate soundly more effect-based program equivalences than would be possible with previous semantics. Our semantics uses 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 generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves twoawkward problems caused by naïve use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.

Supplementary Material

JPG File (d3_right_t6.jpg)

Download
11.28 KB

MP4 File (d3_right_t6.mp4)

Download
420.21 MB

References

[1]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009.

Digital Library

[2]

G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Program., 13(2):261--293, 2003.

Digital Library

[3]

N. Benton, L. Beringer, M. Hofmann, and A. Kennedy. Relational semantics for effect-based program transformations: higher-order store. In PPDP, 2009.

Digital Library

[4]

N. Benton, M. Hofmann, and V. Nigam. Proof-relevant logical relations for name generation. In TLCA, 2013.

[5]

N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP, 2009.

Digital Library

[6]

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-based program transformations with dynamic allocation. In PPDP, 2007.

Digital Library

[7]

N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations. In APLAS, volume 4279 of LNCS, 2006.

Digital Library

[8]

N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In ICFP, 1998.

Digital Library

[9]

N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In TLCA, volume 3461 of LNCS, 2005.

Digital Library

[10]

L. Birkedal, A. Carboni, G. Rosolini, and D. S. Scott. Type theory via exact categories. In LICS, 1998.

Digital Library

[11]

L. Birkedal, K. Stovring, and J. Thamsborg. The category-theoretic solution of recursive metric-space equations. Theor. Comp. Sci., 411:4102--4122, 2010.

Digital Library

[12]

G. Boudol. Typing termination in a higher-order concurrent imperative language. Inf. Comput., 208(6), 2010.

Digital Library

[13]

C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In LICS, pages 366--378, 2007.

Digital Library

[14]

A. Carboni, P. J. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In MFPS, LNCS 298, 1987.

Digital Library

[15]

Y. Cheon, G. T. Leavens, M. Sitaraman, and S. H. Edwards. Model variables: cleanly supporting abstraction in design by contract. Softw., Pract. Exper., 35(6):583--599, 2005.

Digital Library

[16]

W. P. de Roever and K. Engelhardt. Data Refinement: Model-oriented Proof Theories and their Comparison. Cambridge University Press, 1998.

Digital Library

[17]

T. Dinsdale-Young, P. Gardner, and M. J. Wheelhouse. Abstraction and refinement for local reasoning. In VSTTE, volume 6217 of LNCS, 2010.

Digital Library

[18]

D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. Logical Methods in Computer Science, 7(2), 2011.

[19]

D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In Proc. ICFP, ACM, pages 143--156, 2010.

Digital Library

[20]

J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. In POPL, pages 233--246, 2005.

Digital Library

[21]

M. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3--5):341--363, 2002.

[22]

D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In LISP and Functional Programming, 1986.

Digital Library

[23]

C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011.

Digital Library

[24]

C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and kripke logical relations. In J. Field and M. Hicks, editors, POPL, pages 59--72. ACM, 2012.

Digital Library

[25]

J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP, volume 7211 of LNCS, 2012.

Digital Library

[26]

O. Kammar and G. D. Plotkin. Algebraic foundations for effect-dependent optimisations. In POPL, 2012.

Digital Library

[27]

V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, 2006.

Digital Library

[28]

N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In TLDI, 2010.

Digital Library

[29]

N. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In ICFP, 2012.

Digital Library

[30]

R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL, 2013.

Digital Library

[31]

S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer, 2nd edition, Sept. 1998.

[32]

B. Meyer. Applying "design by contract". IEEE Computer, 25(10):40--51, 1992.

Digital Library

[33]

F. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Carnegie Mellon University, 1982.

Digital Library

[34]

A. Pitts and I. Stark. Operational reasoning for functions with local state. In Higher order operational techniques in semantics, pages 227--273. Cambridge University Press, 1998.

Digital Library

[35]

A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.

Digital Library

[36]

A. M. Pitts and I. D. B. Stark. Observable properties of higher-order functions that dynamically create local names, or what's new? In MFCS, volume 711 of LNCS, 1993.

Digital Library

[37]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.

Digital Library

[38]

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. Logical Methods in Computer Science, 7(3), 2011.

[39]

I. Stark. Names and Higher-Order Functions. PhD thesis, U. Cambridge, 1994.

[40]

E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. In POPL, 2005.

Digital Library

[41]

J. Thamsborg and L. Birkedal. A Kripke logical relation for effect-based program transformations. In ICFP, 2011.

Digital Library

[42]

V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, volume 4703 of LNCS, 2007.

Digital Library

[43]

P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4(1):1--32, 2003.

Digital Library

Cited By

Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Dvir YKammar OLahav O(2024)A Denotational Approach to Release/Acquire ConcurrencyProgramming Languages and Systems10.1007/978-3-031-57267-8_5(121-149)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_5
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Show More Cited By

Index Terms

Abstract effects and proof-relevant logical relations
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Dynamic compilers
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems
        Memory management
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics
      1. Denotational semantics

Recommendations

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, ...
Abstract effects and proof-relevant logical relations
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or ...
Logical Step-Indexed Logical Relations
LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science

We show how to reason about "step-indexed" logical relations in an abstract way, avoiding the tedious, error-prone, and proof-obscuring step-index arithmetic that seems superficially to be an essential element of the method. Specifically, we define a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 1

POPL '14

January 2014

661 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2578855

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2014
702 pages
ISBN:9781450325448
DOI:10.1145/2535838
General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Published in SIGPLAN Volume 49, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
290
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Dvir YKammar OLahav O(2024)A Denotational Approach to Release/Acquire ConcurrencyProgramming Languages and Systems10.1007/978-3-031-57267-8_5(121-149)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_5
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Aguirre ABarthe GGaboardi MGarg DKatsumata SSato T(2021)Higher-order probabilistic adversarial computations: categorical semantics and program logicsProceedings of the ACM on Programming Languages10.1145/34735985:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473598
QU WGABOARDI MGARG D(2021)Relational cost analysis in a functional-imperative settingJournal of Functional Programming10.1017/S095679682100007131Online publication date: 2-Nov-2021
https://doi.org/10.1017/S0956796821000071
Maillard KHriţcu CRivas EVan Muylder A(2019)The next 700 relational program logicsProceedings of the ACM on Programming Languages10.1145/33710724:POPL(1-33)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371072
Simpson AVoorneveld N(2019)Behavioural Equivalence via Modalities for Algebraic EffectsACM Transactions on Programming Languages and Systems10.1145/336351842:1(1-45)Online publication date: 21-Nov-2019
https://dl.acm.org/doi/10.1145/3363518
Qu WGaboardi MGarg D(2019)Relational cost analysis for functional-imperative programsProceedings of the ACM on Programming Languages10.1145/33416963:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341696
Grimm NZanella-Béguelin SMaillard KFournet CHriţcu CMaffei MProtzenko JRamananandro TRastogi ASwamy N(2018)A monadic framework for relational verification: applied to information security, program equivalence, and optimizationsProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167090(130-145)Online publication date: 2018
https://doi.org/10.1145/3176245.3167090
Banerjee ANaumann DNikouei M(2018)A Logical Analysis of Framing for Specifications with Pure Method CallsACM Transactions on Programming Languages and Systems10.1145/317480140:2(1-90)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174801
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents