Skip to content

[spec] Add citation for WasmCert #1533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 20, 2022
Merged

[spec] Add citation for WasmCert #1533

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions document/core/appendix/properties.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -807,7 +807,7 @@ Theorems
~~~~~~~~

Given the definition of :ref:`valid configurations <valid-config>`,
the standard soundness theorems hold. [#cite-cpp2018]_
the standard soundness theorems hold. [#cite-cpp2018]_ [#cite-fm2021]_

**Theorem (Preservation).**
If a :ref:`configuration <syntax-config>` :math:`S;T` is :ref:`valid <valid-config>` with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]` (i.e., :math:`\vdashconfig S;T : [t^\ast]`),
Expand Down Expand Up @@ -839,5 +839,9 @@ Consequently, given a :ref:`valid store <valid-store>`, no computation defined b
Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. |PLDI2017|_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.

.. [#cite-cpp2018]
A machine-verified version of the formalization and soundness proof is described in the following article:
A machine-verified version of the formalization and soundness proof of the PLDI 2017 paper is described in the following article:
Conrad Watt. |CPP2018|_. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.

.. [#cite-fm2021]
Machine-verified formalizations and soundness proofs of the semantics from the official specification are described in the following article:
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. |FM2021|_. Proceedings of the 24th International Symposium on Formal Methods (FM 2021). Springer 2021.
4 changes: 4 additions & 0 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@
.. |MediaType| replace:: Media Type
.. _MediaType: https://www.iana.org/assignments/media-types/media-types.xhtml


.. Literature
.. ----------

Expand All @@ -47,6 +48,9 @@
.. |CPP2018| replace:: Mechanising and Verifying the WebAssembly Specification
.. _CPP2018: https://dl.acm.org/citation.cfm?id=3167082

.. |FM2021| replace:: Two Mechanisations of WebAssembly 1.0
.. _FM2021: https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4

.. |TAPL| replace:: Types and Programming Languages
.. _TAPL: https://www.cis.upenn.edu/~bcpierce/tapl/

Expand Down