Skip to content

Commit

Permalink
Update documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@amintimany
amintimany committed Oct 8, 2023
1 parent 7671644 commit 8fc8d17
Show file tree
Hide file tree
Showing 2 changed files with 118 additions and 18 deletions.
97 changes: 97 additions & 0 deletions folders.css
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
/* Demo page styles
-------------------------------------------------------------- */

/* body { */
/* background: #eee; */
/* line-height: 30px; */
/* } */

h2 {
color: #aaa;
font-size: 30px;
line-height: 40px;
font-style: italic;
font-weight: 200;
margin: 40px;
text-align: center;
text-shadow: 1px 1px 1px rgba(255, 255, 255, 0.7);
}

.box {
background: #fff;
border-radius: 2px;
box-shadow: 0 0 50px rgba(0, 0, 0, 0.1);
margin: 30px 5%;
padding: 5%;
}

@media (min-width: 544px) {
.box {
margin: 40px auto;
max-width: 440px;
padding: 40px;
}
}


/* The list style
-------------------------------------------------------------- */

.directory-list ul {
/* font-family: "times new roman", serif; */
margin-left: 10px;
padding-left: 20px;
border-left: 1px dashed #ddd;
}

.directory-list li {
list-style: none;
color: #888;
font-size: 17px;
/* font-style: italic; */
font-weight: normal;
}

.directory-list a {
border-bottom: 1px solid transparent;
color: rgba(31, 31, 174, 0.85);
text-decoration: none;
transition: all 0.2s ease;
}

.directory-list a:hover {
background-color: rgba(0,0,0,0.1);
border-color: #eee;
color: #000;
}

.directory-list .folder,
.directory-list .folder > a {
color: #777;
/* font-weight: bold; */
}


/* The icons
-------------------------------------------------------------- */

.directory-list li:before {
margin-right: 10px;
content: "";
height: 20px;
vertical-align: middle;
width: 20px;
background-repeat: no-repeat;
display: inline-block;
/* file icon by default */
background-image: url("data:image/svg+xml;utf8,<svg xmlns='http://www.w3.org/2000/svg' viewBox='0 0 100 100'><path fill='lightgrey' d='M85.714,42.857V87.5c0,1.487-0.521,2.752-1.562,3.794c-1.042,1.041-2.308,1.562-3.795,1.562H19.643 c-1.488,0-2.753-0.521-3.794-1.562c-1.042-1.042-1.562-2.307-1.562-3.794v-75c0-1.487,0.521-2.752,1.562-3.794 c1.041-1.041,2.306-1.562,3.794-1.562H50V37.5c0,1.488,0.521,2.753,1.562,3.795s2.307,1.562,3.795,1.562H85.714z M85.546,35.714 H57.143V7.311c3.05,0.558,5.505,1.767,7.366,3.627l17.41,17.411C83.78,30.209,84.989,32.665,85.546,35.714z' /></svg>");
background-position: center 2px;
background-size: 60% auto;
}

.directory-list li.folder:before {
/* folder icon if folder class is specified */
background-image: url("data:image/svg+xml;utf8,<svg xmlns='http://www.w3.org/2000/svg' viewBox='0 0 100 100'><path fill='lightblue' d='M96.429,37.5v39.286c0,3.423-1.228,6.361-3.684,8.817c-2.455,2.455-5.395,3.683-8.816,3.683H16.071 c-3.423,0-6.362-1.228-8.817-3.683c-2.456-2.456-3.683-5.395-3.683-8.817V23.214c0-3.422,1.228-6.362,3.683-8.817 c2.455-2.456,5.394-3.683,8.817-3.683h17.857c3.422,0,6.362,1.228,8.817,3.683c2.455,2.455,3.683,5.395,3.683,8.817V25h37.5 c3.422,0,6.361,1.228,8.816,3.683C95.201,31.138,96.429,34.078,96.429,37.5z' /></svg>");
background-position: center top;
background-size: 75% auto;
}
39 changes: 21 additions & 18 deletions index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
<head>
<title>The Logical Essence of Well-Bracketed Control Flow (artifact) </title>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="folders.css" rel="stylesheet" type="text/css" />
<link href="html/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="html/coqdocjs.css" rel="stylesheet" type="text/css"/>
</head>
Expand All @@ -24,20 +25,22 @@
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<h1>The Logical Essence of Well-Bracketed Control Flow (artifact)</h1>
<h3>A Program logic on top of Iris for reasoning about well-bracketed control flow.</h3>
<h1>A Program logic on top of Iris for reasoning about well-bracketed control flow.</h1>
<hr/>
<h3>Links &amp; Downloads:</h3>

<p>The Coq development is organized as follows. The links below open the browsable html version of the corresponding Coq file (produced by the coqdoc tool and enhanced by coqdocjs).</p>

<ul>
<li>
<b>F_mu_ref</b>: Unary and binary logical relations models for F_mu_ref
<hr/>
<h3>The structure of the Coq development:</h3>
<p> The links below open the browsable html version of the corresponding Coq file (produced by the coqdoc tool and enhanced by coqdocjs). The Coq development is organized as follows.</p>
<ul class="directory-list">
<li class="folder">
<b>F_mu_ref</b>: Unary and binary logical relations models for F_mu_ref.
<ul>
<li><a href="html/WBLogic.F_mu_ref.base.html">base.v</a>: Some basic definitions and tactics.</li>
<li><b>binary</b>: The binary logical relations model.
<li class="folder"><b>binary</b>: The binary logical relations model.
<ul>
<li><a href="html/WBLogic.F_mu_ref.binary.context_refinement.html">context_refinement.v</a>: The definition of contextual refinement and some lemmas.</li>
<li><b>examples</b>: Examples of using our binary loical relatons model.
<li class="folder"><b>examples</b>: Examples of using our binary loical relatons model.
<ul>
<li><a href="html/WBLogic.F_mu_ref.binary.examples.fact.html">fact.v</a>: Equivalnece of two factorial implementations.</li>
<li><a href="html/WBLogic.F_mu_ref.binary.examples.very_awkward.html">very_awkward.v</a>: The contextual equivalence of VAE.</li>
Expand All @@ -51,9 +54,9 @@ <h3>A Program logic on top of Iris for reasoning about well-bracketed control fl
</li>
<li><a href="html/WBLogic.F_mu_ref.lang.html">lang.v</a>: The definition (syntax & op sem) of F_mu_ref.</li>
<li><a href="html/WBLogic.F_mu_ref.typing.html">typing.v</a>: The typing rules of F_mu_ref.</li>
<li><b>unary</b>: The unary logical relations model.
<li class="folder"><b>unary</b>: The unary logical relations model.
<ul>
<li><b>examples</b>: Examples of using our unary loical relatons model.
<li class="folder"><b>examples</b>: Examples of using our unary loical relatons model.
<ul>
<li><a href="html/WBLogic.F_mu_ref.unary.examples.very_awkward.html">very_awkward.v</a>: The VAE example using the unary logical relations.</li>
</ul>
Expand All @@ -66,24 +69,24 @@ <h3>A Program logic on top of Iris for reasoning about well-bracketed control fl
<li><a href="html/WBLogic.F_mu_ref.wp_rules.html">wp_rules.v</a>: The (well-bracketed) weakest precondition rules for F_mu_ref.</li>
</ul>
</li>
<li><b>heap_lang</b>: A copy of the necessary parts of heap lang from the Iris development.
<li class="folder"><b>heap_lang</b>: A copy of the necessary parts of heap lang from the Iris development.
<ul>
<li><a href="html/WBLogic.heap_lang.adequacy.html">adequacy.v</a>: The adequcy theorem.</li>
<li><a href="html/WBLogic.heap_lang.derived_laws.html">derived_laws.v</a>: Derived rules for well-bracketed weakest preconditions.</li>
<li><a href="html/WBLogic.heap_lang.primitive_laws.html">primitive_laws.v</a>: Primitive rules for wekaest preconditions.</li>
<li><a href="html/WBLogic.heap_lang.proofmode.html">proofmode.v</a>: Lemmas and tacktis for proofmode support for heap_lang programs.</li>
</ul>
</li>
<li><b>heap_lang_examples</b>: Examples on top of heap lang.
<li class="folder"><b>heap_lang_examples</b>: Examples on top of heap lang.
<ul>
<li><a href="html/WBLogic.heap_lang_examples.awkward.html">awkward.v</a>: The awkward example.</li>
<li><b>sts</b>: Examples using the STS encoding.
<li class="folder"><b>sts</b>: Examples using the STS encoding.
<ul><li><a href="html/WBLogic.heap_lang_examples.sts.very_awkward.html">very_awkward.v</a>: The STS verion of VAE.</li></ul>
</li>
<li><a href="html/WBLogic.heap_lang_examples.very_awkward.html">very_awkward.v</a>: VAE proven well-bracketed in heap lang.</li>
</ul>
</li>
<li><b>heap_lang_trace</b>: The version of heap lang with intensional traces.
<li class="folder"><b>heap_lang_trace</b>: The version of heap lang with intensional traces.
<ul>
<li><a href="html/WBLogic.heap_lang_trace.adequacy.html">adequacy.v</a>: The adequacy theorem.</li>
<li><a href="html/WBLogic.heap_lang_trace.class_instances.html">class_instances.v</a>: Type classes for Iris's proof mode.</li>
Expand All @@ -96,19 +99,19 @@ <h3>A Program logic on top of Iris for reasoning about well-bracketed control fl
<li><a href="html/WBLogic.heap_lang_trace.trace_resources.html">trace_resources.v</a>: Iris resources for reasoning about program traces.</li>
</ul>
</li>
<li><b>heap_lang_trace_examples</b>: Examples using intensional trace properties in heap lang.
<li class="folder"><b>heap_lang_trace_examples</b>: Examples using intensional trace properties in heap lang.
<ul>
<li><a href="html/WBLogic.heap_lang_trace_examples.sequential_trace_alt.html">sequential_trace_alt.v</a>: The definition of well-bracketed trace of calls and returns.</li>
<li><a href="html/WBLogic.heap_lang_trace_examples.very_awkward.html">very_awkward.v</a>: The VAE example proven to produce well-bracketed traces.</li>
</ul>
</li>
<li><a href="html/WBLogic.oneshot.html">oneshot.v</a>: The definition of the one-shot resource algebra</li>
<li><a href="html/WBLogic.persistent_pred.html">persistent_pred.v</a>: Definition of persistent predicates used in logical relations.</li>
<li><b>program_logic</b>: The well-bracketed program logic.
<li class="folder"><b>program_logic</b>: The well-bracketed program logic.
<ul>
<li><a href="html/WBLogic.program_logic.adequacy.html">adequacy.v</a>: The adequacy theorem of the well-bracketed program logic.</li>
<li><a href="html/WBLogic.program_logic.ghost_stacks.html">ghost_stacks.v</a>: The theory of ghost stacks including resource algebras.</li>
<li><b>lib</b>: Developments on top of the well-bracketed program logic.
<li class="folder"><b>lib</b>: Developments on top of the well-bracketed program logic.
<ul><li><a href="html/WBLogic.program_logic.lib.sts.html">sts.v</a>: The encoding of STSs using ghost stacks.</li></ul>
</li>
<li><a href="html/WBLogic.program_logic.lifting.html">lifting.v</a>: A couple of useful lemmas.</li>
Expand Down

0 comments on commit 8fc8d17

Please sign in to comment.