Aarhus University Seal / Aarhus Universitets segl

A semantic foundation for hidden state

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Jan Schwinghammer, Saarland Univ., Germany
  • Hongseok Yang, Queen Mary Univ. of London, United Kingdom
  • Lars Birkedal
  • François Pottier, INRIA Institut National de Rechereche en Informatique et en Automatique, France
  • Bernhard Reus, Univ. of Sussex, United Kingdom

We present the first complete soundness proof of the antiframe rule, a recently proposed proof rule for capturing information hiding in the presence of higher-order store. Our proof involves solving a non-trivial recursive domain equation, and it helps identify some of the key ingredients for soundness.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures : 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
EditorsLuke Ong
Number of pages16
PublisherSpringer
Publication year30 Apr 2010
Pages2-17
ISBN (print)9783642120312
ISBN (Electronic)978-3-642-12032-9
DOIs
Publication statusPublished - 30 Apr 2010
Externally publishedYes
SeriesLecture Notes in Computer Science
Volume6014
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 81389029