Commit 3e4c74eb authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

website for Shadow_SC_DOM

parent 97e390b29fa8
......@@ -8359,6 +8359,31 @@ abstract =
allows them to make more assumptions about other code accessing the
DOM.
 
[Shadow_SC_DOM]
title = A Formal Model of the Safely Composable Document Object Model with Shadow Roots
author = Achim D. Brucker <https://www.brucker.ch>, Michael Herzberg <http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg>
topic = Computer science/Data structures
date = 2020-09-28
notify = adbrucker@0x5f.org, mail@michael-herzberg.de
abstract =
In this AFP entry, we extend our formalization of the safely
composable DOM with Shadow Roots. This is a proposal for Shadow Roots
with stricter safety guarantess than the standard compliant
formalization (see "Shadow DOM"). Shadow Roots are a recent
proposal of the web community to support a component-based development
approach for client-side web applications. Shadow roots are a
significant extension to the DOM standard and, as web standards are
condemned to be backward compatible, such extensions often result in
complex specification that may contain unwanted subtleties that can be
detected by a formalization. Our Isabelle/HOL formalization is, in
the sense of object-orientation, an extension of our formalization of
the core DOM and enjoys the same basic properties, i.e., it is
extensible, i.e., can be extended without the need of re-proving
already proven properties and executable, i.e., we can generate
executable code from our specification. We exploit the executability
to show that our formalization complies to the official standard of
the W3C, respectively, the WHATWG.
[Store_Buffer_Reduction]
title = A Reduction Theorem for Store Buffers
author = Ernie Cohen <mailto:ecohen@amazon.com>, Norbert Schirmer <mailto:norbert.schirmer@web.de>
......
......@@ -150,7 +150,9 @@ DOM.</td>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Shadow_SC_DOM.html">Shadow_SC_DOM</a> </td></tr>
</tbody>
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>A Formal Model of the Safely Composable Document Object Model with Shadow Roots - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">A</font>
<font class="first">F</font>ormal
<font class="first">M</font>odel
of
the
<font class="first">S</font>afely
<font class="first">C</font>omposable
<font class="first">D</font>ocument
<font class="first">O</font>bject
<font class="first">M</font>odel
with
<font class="first">S</font>hadow
<font class="first">R</font>oots
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">A Formal Model of the Safely Composable Document Object Model with Shadow Roots</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
Achim D. Brucker (a /dot/ brucker /at/ exeter /dot/ ac /dot/ uk) and
<a href="http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg">Michael Herzberg</a>
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2020-09-28</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
In this AFP entry, we extend our formalization of the safely
composable DOM with Shadow Roots. This is a proposal for Shadow Roots
with stricter safety guarantess than the standard compliant
formalization (see "Shadow DOM"). Shadow Roots are a recent
proposal of the web community to support a component-based development
approach for client-side web applications. Shadow roots are a
significant extension to the DOM standard and, as web standards are
condemned to be backward compatible, such extensions often result in
complex specification that may contain unwanted subtleties that can be
detected by a formalization. Our Isabelle/HOL formalization is, in
the sense of object-orientation, an extension of our formalization of
the core DOM and enjoys the same basic properties, i.e., it is
extensible, i.e., can be extended without the need of re-proving
already proven properties and executable, i.e., we can generate
executable code from our specification. We exploit the executability
to show that our formalization complies to the official standard of
the W3C, respectively, the WHATWG.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Shadow_SC_DOM-AFP,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formal Model of the Safely Composable Document Object Model with Shadow Roots},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
note = {\url{http://isa-afp.org/entries/Shadow_SC_DOM.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Core_SC_DOM.html">Core_SC_DOM</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Shadow_SC_DOM/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Shadow_SC_DOM/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Shadow_SC_DOM/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Shadow_SC_DOM-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -114,6 +114,15 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<a href="https://www-users.cs.york.ac.uk/~simonf/">Simon Foster</a>
and <a href="https://www.lri.fr/~wolff/">Burkhart Wolff</a>
</td>
</tr>
<tr>
<td class="entry">
2020-09-28: <a href="entries/Shadow_SC_DOM.html">A Formal Model of the Safely Composable Document Object Model with Shadow Roots</a>
<br>
Authors:
Achim D. Brucker
and <a href="http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg">Michael Herzberg</a>
</td>
</tr>
<tr>
<td class="entry">
......
......@@ -62,6 +62,31 @@ construction is validated by a test-set of known equivalences between
both quantities and SI units. Moreover, the presented theory can be
used for type-safe conversions between the SI system and others, like
the British Imperial System (BIS).</description>
</item>
<item>
<title>A Formal Model of the Safely Composable Document Object Model with Shadow Roots</title>
<link>https://www.isa-afp.org/entries/Shadow_SC_DOM.html</link>
<guid>https://www.isa-afp.org/entries/Shadow_SC_DOM.html</guid>
<dc:creator> Achim D. Brucker, Michael Herzberg </dc:creator>
<pubDate>28 Sep 2020 00:00:00 +0000</pubDate>
<description>
In this AFP entry, we extend our formalization of the safely
composable DOM with Shadow Roots. This is a proposal for Shadow Roots
with stricter safety guarantess than the standard compliant
formalization (see &#34;Shadow DOM&#34;). Shadow Roots are a recent
proposal of the web community to support a component-based development
approach for client-side web applications. Shadow roots are a
significant extension to the DOM standard and, as web standards are
condemned to be backward compatible, such extensions often result in
complex specification that may contain unwanted subtleties that can be
detected by a formalization. Our Isabelle/HOL formalization is, in
the sense of object-orientation, an extension of our formalization of
the core DOM and enjoys the same basic properties, i.e., it is
extensible, i.e., can be extended without the need of re-proving
already proven properties and executable, i.e., we can generate
executable code from our specification. We exploit the executability
to show that our formalization complies to the official standard of
the W3C, respectively, the WHATWG.</description>
</item>
<item>
<title>The Safely Composable DOM</title>
......@@ -565,52 +590,5 @@ connection between the notion of Attack Tree validity and CTL. The
application is illustrated on the example of a healthcare IoT system
and GDPR compliance verification.</description>
</item>
<item>
<title>Power Sum Polynomials</title>
<link>https://www.isa-afp.org/entries/Power_Sum_Polynomials.html</link>
<guid>https://www.isa-afp.org/entries/Power_Sum_Polynomials.html</guid>
<dc:creator> Manuel Eberl </dc:creator>
<pubDate>24 Apr 2020 00:00:00 +0000</pubDate>
<description>
&lt;p&gt;This article provides a formalisation of the symmetric
multivariate polynomials known as &lt;em&gt;power sum
polynomials&lt;/em&gt;. These are of the form
p&lt;sub&gt;n&lt;/sub&gt;(&lt;em&gt;X&lt;/em&gt;&lt;sub&gt;1&lt;/sub&gt;,&amp;hellip;,
&lt;em&gt;X&lt;/em&gt;&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt;) =
&lt;em&gt;X&lt;/em&gt;&lt;sub&gt;1&lt;/sub&gt;&lt;sup&gt;n&lt;/sup&gt;
+ &amp;hellip; +
X&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt;&lt;sup&gt;n&lt;/sup&gt;.
A formal proof of the Girard–Newton Theorem is also given. This
theorem relates the power sum polynomials to the elementary symmetric
polynomials s&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt; in the form
of a recurrence relation
(-1)&lt;sup&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sup&gt;
&lt;em&gt;k&lt;/em&gt; s&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt;
=
&amp;sum;&lt;sub&gt;i&amp;isinv;[0,&lt;em&gt;k&lt;/em&gt;)&lt;/sub&gt;
(-1)&lt;sup&gt;i&lt;/sup&gt; s&lt;sub&gt;i&lt;/sub&gt;
p&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;-&lt;em&gt;i&lt;/em&gt;&lt;/sub&gt;&amp;thinsp;.&lt;/p&gt;
&lt;p&gt;As an application, this is then used to solve a generalised
form of a puzzle given as an exercise in Dummit and Foote&#39;s
&lt;em&gt;Abstract Algebra&lt;/em&gt;: For &lt;em&gt;k&lt;/em&gt;
complex unknowns &lt;em&gt;x&lt;/em&gt;&lt;sub&gt;1&lt;/sub&gt;,
&amp;hellip;,
&lt;em&gt;x&lt;/em&gt;&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt;,
define p&lt;sub&gt;&lt;em&gt;j&lt;/em&gt;&lt;/sub&gt; :=
&lt;em&gt;x&lt;/em&gt;&lt;sub&gt;1&lt;/sub&gt;&lt;sup&gt;&lt;em&gt;j&lt;/em&gt;&lt;/sup&gt;
+ &amp;hellip; +
&lt;em&gt;x&lt;/em&gt;&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt;&lt;sup&gt;&lt;em&gt;j&lt;/em&gt;&lt;/sup&gt;.
Then for each vector &lt;em&gt;a&lt;/em&gt; &amp;isinv;
&amp;#x2102;&lt;sup&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sup&gt;, show that
there is exactly one solution to the system p&lt;sub&gt;1&lt;/sub&gt;
= a&lt;sub&gt;1&lt;/sub&gt;, &amp;hellip;,
p&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt; =
a&lt;sub&gt;&lt;em&gt;k&lt;/em&gt;&lt;/sub&gt; up to permutation of
the
&lt;em&gt;x&lt;/em&gt;&lt;sub&gt;&lt;em&gt;i&lt;/em&gt;&lt;/sub&gt;
and determine the value of
p&lt;sub&gt;&lt;em&gt;i&lt;/em&gt;&lt;/sub&gt; for
i&amp;gt;k.&lt;/p&gt;</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -281,6 +281,7 @@
<a href="entries/Optimal_BST.html">Optimal_BST</a> &nbsp;
<a href="entries/Core_DOM.html">Core_DOM</a> &nbsp;
<a href="entries/Core_SC_DOM.html">Core_SC_DOM</a> &nbsp;
<a href="entries/Shadow_SC_DOM.html">Shadow_SC_DOM</a> &nbsp;
<a href="entries/Auto2_Imperative_HOL.html">Auto2_Imperative_HOL</a> &nbsp;
<a href="entries/IMP2_Binary_Heap.html">IMP2_Binary_Heap</a> &nbsp;
<a href="entries/Priority_Search_Trees.html">Priority_Search_Trees</a> &nbsp;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment