Skip to content

Commit

Permalink
update page
Browse files Browse the repository at this point in the history
  • Loading branch information
@ranjitjhala
ranjitjhala committed Jun 23, 2017
1 parent 92f98b7 commit 099e7ef
Show file tree
Hide file tree
Showing 6 changed files with 35 additions and 35 deletions.
18 changes: 9 additions & 9 deletions docs/120/03-datatypes.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,9 +213,10 @@
</div>

</div>
<section id="data-types" class="level1">
<h1>Data Types</h1>
<section id="data-types" class="level2">
<h2>Data Types</h2>
<p><br></p>
</section>
<section id="example-lists" class="level2">
<h2>Example: Lists</h2>
<p><br></p>
Expand Down Expand Up @@ -263,10 +264,10 @@ <h2>Specifying the size of a List</h2>
(:::) :: x:a -&gt; xs:List a -&gt; {v:List a|size v = 1 + size xs}
</code></pre>
</section>
</section>
<section id="using-measures" class="level1">
<h1>Using Measures</h1>
<section id="using-measures" class="level2">
<h2>Using Measures</h2>
<p><br></p>
</section>
<section id="exercise-partial-functions" class="level2">
<h2>Exercise: <em>Partial</em> Functions</h2>
<p><br></p>
Expand Down Expand Up @@ -372,12 +373,12 @@ <h2>Exercise: <code>average</code></h2>
<p><strong>Q:</strong> What is a safe input type for <code>average'</code>?</p>
<p><br></p>
</section>
</section>
<section id="refining-data-types" class="level1">
<h1>Refining Data Types</h1>
<section id="refining-data-types" class="level2">
<h2>Refining Data Types</h2>
<p><br> <br></p>
<p>    <em>Make illegal states unrepresentable</em></p>
<p><br></p>
</section>
<section id="example-year-is-12-months" class="level2">
<h2>Example: Year is 12 Months</h2>
<p><br></p>
Expand Down Expand Up @@ -565,7 +566,6 @@ <h2>Recap</h2>
<li><a href="06-case-study-bytestring.html">Low-level Memory</a></li>
</ul>
</section>
</section>

</div>
</div>
Expand Down
28 changes: 14 additions & 14 deletions docs/120/04-case-study-insertsort.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,9 +215,10 @@

</div>
<p><br></p>
<section id="case-study-insertion-sort" class="level1">
<h1>Case Study: Insertion Sort</h1>
<section id="case-study-insertion-sort" class="level2">
<h2>Case Study: Insertion Sort</h2>
<p><br></p>
</section>
<section id="asdisort" class="level2">
<h2>Insertion Sort</h2>
<p><br></p>
Expand All @@ -242,10 +243,10 @@ <h2>Goal: Verified Insertion Sort</h2>
<p>Has the same <strong>elements</strong> as the input,</p>
<p>Is in increasing <strong>order</strong>.</p>
</section>
</section>
<section id="property-1-size" class="level1">
<h1>Property 1: Size</h1>
<section id="property-1-size" class="level2">
<h2>Property 1: Size</h2>
<p><br></p>
</section>
<section id="exercise-insert" class="level2">
<h2>Exercise: <code>insert</code></h2>
<p><br></p>
Expand All @@ -271,10 +272,10 @@ <h2>Exercise: <code>insert</code></h2>

<p><br></p>
</section>
</section>
<section id="property-2-elements" class="level1">
<h1>Property 2: Elements</h1>
<section id="property-2-elements" class="level2">
<h2>Property 2: Elements</h2>
<p><br></p>
</section>
<section id="permutation" class="level2">
<h2>Permutation</h2>
<p><br></p>
Expand Down Expand Up @@ -341,14 +342,14 @@ <h2>Exercise: Verifying Permutation</h2>

<p><strong>Q:</strong> Can you fix the type for <code>insertE</code> so <code>sortE</code> verifies?</p>
</section>
</section>
<section id="property-3-order" class="level1">
<h1>Property 3: Order</h1>
<section id="property-3-order" class="level2">
<h2>Property 3: Order</h2>
<p><br></p>
<p>Yes, yes, but does <code>sort</code> actually <strong>sort</strong> ?</p>
<p><br></p>
<p>How to specify <strong>ordered lists</strong> ?</p>
<p><br></p>
</section>
<section id="recall-refined-data-types" class="level2">
<h2>Recall: Refined Data Types</h2>
<p><br></p>
Expand Down Expand Up @@ -540,9 +541,9 @@ <h2>Exercise: Insertion Sort</h2>
</div>

</section>
<section id="multiple-measures" class="level2">
<h2>Multiple Measures</h2>
</section>
<section id="multiple-measures" class="level1">
<h1>Multiple Measures</h1>
<section id="different-measures-for-list" class="level2">
<h2>Different Measures for <code>List</code></h2>
<p><br></p>
Expand Down Expand Up @@ -602,7 +603,6 @@ <h2>Continue</h2>
<p><br></p>
<p><strong>Continue:</strong> <a href="05-termination.html">[Part II : Proofs]</a></p>
</section>
</section>

</div>
</div>
Expand Down
6 changes: 3 additions & 3 deletions docs/120/05-termination.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,9 +193,10 @@
</div>

</div>
<section id="termination-checking" class="level1">
<h1>Termination Checking</h1>
<section id="termination-checking" class="level2">
<h2>Termination Checking</h2>
<p><br></p>
</section>
<section id="why-termination-checking" class="level2">
<h2>Why termination Checking?</h2>
<p><br> <br></p>
Expand Down Expand Up @@ -539,7 +540,6 @@ <h2>What properties can be expressed in the logic?</h2>
<p><strong>Next: <em>Any</em> Terminating Haskell Function</strong></p>
<p><a href="06-reflection.html">Refinement Reflection</a></p>
</section>
</section>

</div>
</div>
Expand Down
6 changes: 3 additions & 3 deletions docs/120/06-reflection.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -205,9 +205,10 @@

</div>
<p><br> <br> <br> <br> <br></p>
<section id="refinement-reflection" class="level1">
<h1>Refinement Reflection</h1>
<section id="refinement-reflection" class="level2">
<h2>Refinement Reflection</h2>
<p><br> <br> Allow terminating <strong>Haskell</strong> functions in refinements!</p>
</section>
<section id="theorems-about-haskell-functions" class="level2">
<h2>Theorems about Haskell functions</h2>
<p><br></p>
Expand Down Expand Up @@ -585,7 +586,6 @@ <h2>Recap</h2>
<p><br></p>
<p><strong>Next:</strong> <a href="07-structural-induction.html">Structural Induction</a>: Program Properties about data types!</p>
</section>
</section>

</div>
</div>
Expand Down
6 changes: 3 additions & 3 deletions docs/120/07-structural-induction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,9 +204,10 @@

</div>
<p><br> <br> <br> <br> <br></p>
<section id="structural-induction" class="level1">
<h1>Structural Induction</h1>
<section id="structural-induction" class="level2">
<h2>Structural Induction</h2>
<p><br> <br> How we <em>express</em> and <em>prove</em> properties on data types? <br></p>
</section>
<section id="the-list-data-type" class="level2">
<h2>The list data type</h2>
<p><br> A user defined list, <br></p>
Expand Down Expand Up @@ -642,7 +643,6 @@ <h2>Monoid Laws: Associativity</h2>
&&& associativity xs f g</div>
</div>

</section>
</section>

</div>
Expand Down
6 changes: 3 additions & 3 deletions docs/120/08-case-study-map-reduce.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -209,12 +209,13 @@
</div>

</div>
<section id="case-study-mapreduce" class="level1">
<h1>Case Study: MapReduce</h1>
<section id="case-study-mapreduce" class="level2">
<h2>Case Study: MapReduce</h2>
<p><br> Chunk input, map operation (in parallel), and reduce the results. <br> <br></p>
<p align="center">
<img src="img/map-reduce.jpg" height=350px/>
</p>
</section>
<section id="mapreduce-library" class="level2">
<h2>MapReduce &quot;Library&quot;</h2>
<p><br> Haskell definition and reflection <br></p>
Expand Down Expand Up @@ -626,7 +627,6 @@ <h2>List Manipulation</h2>
(C x xs) ++ ys = x `C` (xs ++ ys)</div>
</div>

</section>
</section>

</div>
Expand Down

0 comments on commit 099e7ef

Please sign in to comment.