ucsd-progsys · nikivazou · Oct 25, 2017 · Oct 26, 2017 · Oct 26, 2017 · Oct 26, 2017
diff --git a/Makefile b/Makefile
@@ -1,7 +1,7 @@
 
 
 ##############################################
-TALK=120
+TALK=reflection
 ##############################################
 SRC=src-$(TALK)
 ##############################################

diff --git a/README.md b/README.md
@@ -9,6 +9,7 @@ on programming and proving with Refinement types with [LiquidHaskell][lh-github]
 
 For other versions, you may be interested in:
 
++ [Reflection](http://ucsd-progsys.github.io/intro-refinement-types/reflection/)
 + [25 mins](http://ucsd-progsys.github.io/intro-refinement-types/25/)
 + [2 Hr Workshop](http://ucsd-progsys.github.io/lh-workshop/)
 + [Tutorial](http://ucsd-progsys.github.io/liquidhaskell-tutorial/)

diff --git a/assets/img/benchmarks.png b/assets/img/benchmarks.png
diff --git a/assets/img/or-nat.png b/assets/img/or-nat.png
diff --git a/assets/img/or-type.png b/assets/img/or-type.png
diff --git a/assets/img/props-as-types.png b/assets/img/props-as-types.png
diff --git a/docs/reflection/01-index.html b/docs/reflection/01-index.html
@@ -0,0 +1,319 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="utf-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <meta name="generator" content="rustdoc">
+    <title>An Introduction to Refinement Types</title>
+
+    <link href="./css/bootstrap.css" rel="stylesheet">
+    <link href="./css/bootstrap-theme.css" rel="stylesheet">
+    <link rel="stylesheet" type="text/css" href="./css/rust-book-slides.css">
+    <link rel="stylesheet" type="text/css" href="./css/editor-slides.css">
+    <link rel="stylesheet" type="text/css" href="./css/code-format.css">
+    <link rel="stylesheet" type="text/css" href="./css/slideshow.css">
+    <link rel="stylesheet" type="text/css" href="./css/onepage-scroll.css">
+    <style>
+
+      html {
+            height: 100%;
+      }
+
+      .wrapper {
+            height: 100% !important;
+            height: 100%;
+            margin: 0 auto;
+            overflow: hidden;
+      }
+
+      .main section  {
+            overflow: hidden;
+      }
+
+
+      body {
+        text-align: center;
+      }
+      .mybreak {
+        line-height: 1em;
+      }
+      table {
+        margin-left: 150px;
+        margin-right: auto;
+      }
+
+      ul {
+          list-style-type: none;
+        }
+
+      #slide-nav {
+          position: absolute;
+          bottom: 4%;
+          /* left: 40%; */
+          right: 4%;
+          z-index: 100;
+      }
+
+      #checker-status {
+          position: absolute;
+          top: 4%;
+          right: 2%;
+      }
+
+    </style>
+
+
+      <!-- JQUERY LOCAL
+
+        <script type="text/javascript" src="./js/jquery/jquery-2.0.3.min.js"></script>
+
+      -->
+
+     <!-- JQUERY MOBILE -->
+
+     <!-- Include the jQuery library -->
+     <script src="./js/jquery/jquery-1.11.3.min.js"></script>
+
+     <!-- SWIPE
+       <script src="./js/jquery/init-mobile.js"></script>
+       <script src="./js/jquery/jquery.mobile-1.4.5.min.js"></script>
+     -->
+
+
+
+<script type="text/javascript" src="./js/angular/angular.js"></script>
+<script type="text/javascript" src="./js/bootstrap/bootstrap.js"></script>
+<script type="text/javascript" src="./js/liquid/onepagescroll.js"></script>
+
+<script type="text/x-mathjax-config">
+MathJax.Hub.Config({
+  TeX: {
+    extensions: ["color.js"],
+    Macros: {
+      True: "\\mathit{True}",
+      RR:   "{\\bf R}",
+      Int:  "\\mathtt{Int}",
+      Nat:  "\\mathtt{Nat}",
+      Zero: "\\mathtt{Zero}",
+      foo:   ["{\\bf Jhala FOO #1}", 1],
+      kvar:  ["{\\color[rgb]{1,0,0}{K_{#1}({#2})}}", 2],
+      bindx: ["{{#1}\\!:\\!{#2}}", 2],
+      reft:  ["\\{\\bindx{#1}{#2} \\mid {#3}\\}", 3],
+      ereft: ["\\bindx{#1}{\\{#2 \\mid #3\\}}", 3],
+      reftx: ["\\{{#1}\\mid{#2}\\}", 2],
+      inferrule: ["\\frac{#2}{#3}\\;{#1}", 3]
+  }
+  }
+});
+</script>
+
+<!-- GITHUB -->
+<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>
+
+<!-- LOCAL
+
+  <script src="js/MathJax-2.6.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>
+
+-->
+
+</head>
+
+<body class="rustdoc" data-spy="scroll" data-target=".bs-docs-sidebar" ng-app="liquidDemo" ng-controller="LiquidDemoCtrl">
+
+
+
+<div id='toc' class='mobile-hidden'>
+
+</div>
+
+       <div id="checker-status">
+
+         <!-- Verifying ... -->
+         <button class="btn btn-xs btn-link actbutton" type="button" style="font-size:30px; z-index:1"
+                ng-show="isChecking" ng-click="verifySource()">
+          <span class="glyphicon glyphicon-hourglass"></span>
+         </button>
+
+
+         <!-- Safe -->
+         <button class="btn btn-xs btn-link actbutton" type="button" style="font-size:30px; color:green; z-index:1"
+                 ng-show="isSafe">
+           <span class="glyphicon glyphicon-ok"></span>
+         </button>
+
+         <div class="dropdown" ng-show="isBad">
+             <button class="btn btn-xs btn-link dropdown-toggle"
+                     type="button"
+                     id="errorblockdropdown"
+                     data-toggle="dropdown"
+                     style="font-size:30px; color:red; z-index:1">
+               <span class="glyphicon glyphicon-remove" style="vertical-align:middle"></span><font size="4">{{errorBlocks.length}}</font>
+               </span>
+             </button>
+             <ul class="dropdown-menu" role="menu" aria-labelledby="dLabel">
+               <li ng-repeat="err in errorBlocks">
+                 <a tabindex="-1" ng-click="jumpToProgPane(err)">{{err.index}}</a>
+               </li>
+             </ul>
+         </div>
+       </div>
+
+
+<div class="wrapper">
+<div class="main">
+
+
+<div class="hidden">
+<div id="program-pane-0" class="welleditor" style="background:#fff; position:relative">
+
+  <!-- Verify Source -->
+  <button class="btn btn-xs btn-link actbutton" type="button" style="z-index:1"
+          ng-show="isUnknown" ng-click="verifySource()">
+    <span class="glyphicon glyphicon-play"></span>
+  </button>
+
+  <div id="program-0" class="programbox">module Intro where
+
+dummy :: Int
+dummy = 7</div>
+</div>
+
+</div>
+<section>
+<p><br></p>
+<p align="center">
+<h1 style="border-bottom:none">
+Refinement Reflection: <br> Complete Verification with SMT
+</h1>
+<p><br> <br></p>
+<h4 style="border-bottom:none">
+<i>Niki Vazou <br> (Univerisyt of Maryland)</i>
+</h4>
+</p>
+<p><br> <br> <br></p>
+</section>
+<section id="two-tends-in-program-verification" class="level2">
+<h2>Two Tends in Program Verification</h2>
+<p><br></p>
+<ul>
+<li>Type-Theory-based theorem provers (<em>e.g.,</em> Coq and Agda)</li>
+</ul>
+<p><br></p>
+<ul>
+<li>SMT-based verifiers (<em>e.g.,</em> Dafny and F*)</li>
+</ul>
+<p><br></p>
+</section>
+<section id="type-theory-based-theorem-provers" class="level2">
+<h2>Type-Theory-based theorem provers</h2>
+<p><br></p>
+<ul>
+<li><p>Type level computation to reason about program properties.</p></li>
+<li><p>Supply lemmata or rewrite hints to discharge proofs, ...</p></li>
+<li><p>... even in decidable logics.</p></li>
+</ul>
+</section>
+<section id="smt-based-verifiers" class="level2">
+<h2>SMT-based verifiers</h2>
+<p><br></p>
+<ul>
+<li><p>Automate the verification of programs over decidable theories.</p></li>
+<li><p>Encode user-defined functions with universally-quantified axioms, ...</p></li>
+<li><p>... using incomplete (<em>i.e.,</em> <strong>unpredictable</strong>) heuristics for instantiation.</p></li>
+</ul>
+</section>
+<section id="predictable-smt-automated-verification" class="level2">
+<h2>Predictable &amp; SMT-automated Verification</h2>
+<p><br> <br></p>
+<p><strong>GOAL:</strong> Alternative representation of user-defined functions ...</p>
+<p>... for SMT-decidable (<em>i.e.,</em> <strong>unpredictable</strong>) verification.</p>
+<p><br></p>
+</section>
+<section id="refinement-reflection" class="level2">
+<h2>Refinement Reflection</h2>
+<p><br></p>
+<p>Reflect function definition into its result refined type.</p>
+<p><strong>Consequence:</strong></p>
+<p>Value level function application is also ...</p>
+<p>... &quot;SMT&quot; <strong>predictable</strong> function instantiation.</p>
+</section>
+<section id="outline" class="level2">
+<h2>Outline</h2>
+<p><br></p>
+<p>How far can we go?</p>
+<ul>
+<li><a href="02-reflection.html"><strong>1. Refinement Reflection: Fibonacci</strong></a></li>
+<li><a href="03-map-reduce.html"><strong>2. Case Study: MapReduce Equivalence</strong></a></li>
+<li><a href="04-natural-deduction.html"><strong>3. Encoding Natural Deduction</strong></a></li>
+</ul>
+</section>
+<section id="evaluation" class="level2">
+<h2>Evaluation</h2>
+<p><img src="img/benchmarks.png" height=250px></p>
+</section>
+<section id="conclusion" class="level2">
+<h2>Conclusion</h2>
+<p><br></p>
+<ul>
+<li><p>Refinement Reflection and Proof by Logical Evaluation combined ...</p></li>
+<li><p>... allow for complete verification with SMT-automation, but</p></li>
+<li><p>... don't allow for user interaction,</p></li>
+<li><p>... don't allow for proof certificates.</p></li>
+</ul>
+</section>
+<section id="thank-you" class="level2">
+<h2>Thank you!</h2>
+<p><br></p>
+<p><a href="https://nikivazou.github.io/static/popl18/refinement-reflection.pdf">Refinement Reflection: Complete Verification with SMT</a></p>
+<p>to appear in POPL 2018</p>
+<ul>
+<li><em>by</em> Niki Vazou, Anish Tondwalker, Vikraman Choudhoury,</li>
+<li>Ryan Scott, Ryan Newton, Philip Wadler, and Ranjit Jhala</li>
+</ul>
+</section>
+
+</div>
+</div>
+
+<!--Site Meter
+<div class="hidden">
+  <script type="text/javascript" src="http://s23.sitemeter.com/js/counter.js?site=s23liquidtypes"></script>
+  <noscript>
+    <a href="http://s23.sitemeter.com/stats.asp?site=s23liquidtypes"
+      target="_top">
+      <img src="http://s23.sitemeter.com/meter.asp?site=s23liquidtypes"
+      alt="Site Meter" border="0"/></a>
+  </noscript>
+</div>
+-->
+
+
+
+
+<!-- JavaScript below! ============================================== -->
+
+  <script src="./js/ace/ace.js" type="text/javascript" charset="utf-8"></script>
+  <script src="./js/ace/theme-monokai.js" type="text/javascript" charset="utf-8"></script>
+  <script src="./js/ace/mode-haskell.js"  type="text/javascript" charset="utf-8"></script>
+  <script src="./js/liquid/tooltip.js"></script>
+  <script src="./js/liquid/annot.js"></script>
+  <script src="./js/liquid/config.js"></script>
+  <script src="./js/liquid/slideshow.js"></script>
+  <script src="./js/liquid/liquid.js"></script>
+
+  <script type="text/javascript">
+    var queryServerURL = "http://goto.ucsd.edu:8090/" ;
+  </script>
+
+  <script>
+    onePageScroll(".main", {
+      sectionContainer: "section",
+      loop: true,
+      responsiveFallback: false
+    });
+ </script>
+
+
+
+</body>
+</html>