Skip to content

Commit

Permalink
Add draft of course desc
Browse files Browse the repository at this point in the history
  • Loading branch information
@dbp
dbp committed Mar 17, 2019
1 parent 17bb9ce commit c677167
Show file tree
Hide file tree
Showing 6 changed files with 187 additions and 0 deletions.
68 changes: 68 additions & 0 deletions _site/courses/verifcomp/index.html
View file
@@ -0,0 +1,68 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>dbp.io :: Verified Compilers and Multi-Language Software</title>
<link rel="stylesheet" type="text/css" href="../../css/default.css" />
<link rel="stylesheet" type="text/css" href="../../css/syntax.css" />
</head>
<body>

<h2>Verified Compilers and Multi-Language Software</h2>

<table>
<tbody>
<tr class="odd">
<td align="left">Course</td>
<td>CS4910: Verified Compilers and Multi-Language Software</td>
</tr>
<tr class="even">
<td align="left">Semester</td>
<td>Fall 2019</td>
</tr>
<tr class="odd">
<td align="left">Meeting</td>
<td>Monday/Thursday, 11:45AM-1:25PM</td>
</tr>
<tr class="even">
<td align="left">Instructor</td>
<td>Daniel Patterson (<a href="mailto:dbp@dbpmail.net">dbp@dbpmail.net</a>)</td>
</tr>
<tr class="odd">
<td align="left">Office</td>
<td>WVH 308</td>
</tr>
</tbody>
</table>
<blockquote>
<p>“Can you trust your compiler?” — Xavier Leroy, developer of the Compcert verified C compiler</p>
</blockquote>
<h3 id="why-this-course">Why this course?</h3>
<p>Software is written in a variety of languages, and in many cases, in order to run, it must be compiled down to some lower-level target. <strong>But what if that compiler isn’t correct?</strong> Compilers are some of the trickier pieces of software we build, and yet bugs in them can be insidious, as bugs in compilers means that one of our most basic debugging strategies, reading source code, may not be helpful, since the source may have been miscompiled.</p>
<p>We want, essentially, the compiler to be invisible. But it can only truly be invisible if we can be sure that it does exactly what we expect: if we have proved it correct. Colliding with the field of verified compilation is the question of how different languages should be able to interact – that interaction, or linking, happens after compilation, in the lower-level target language. But the goal is to write source-level programs, not thinking about how our various languages compile, and so again, we want the compiler to be invisible.</p>
<p>These are our high-level motivations. The course itself, while motivated with these problems, will be quite low-level: we will be <strong>building languages, compilers, and proving them correct</strong>.</p>
<h3 id="how-will-the-course-be-structured">How will the course be structured?</h3>
<p><strong>Part 1.</strong> We want to produce verified compilers, and so we will use one of the state-of-the-art tools: the Coq proof assistant. This system allows us to write functional programs and prove properties about them; afterwards we can extract runnable versions of the verified programs. The first section of the course will be dedicated to learning Coq and becoming familiar with the process of <em>mechanized</em> proof – that is, proofs that are checked by a machine. The text that we will use for this section of the course is <a href="https://ilyasergey.net/pnp">“Programs and Proofs” by Ilya Sergey</a>.</p>
<p><strong>Part 2.</strong> This part of the course will involve designing, in groups, different source languages. These will all likely be simple functional languages, and we will do plenty of design review to ensure that the language design you pick will not cause too much difficulty later on.</p>
<p><strong>Part 3.</strong> The final part will involve building and proving correct compilers from your language to a common low-level target language. All the languages will compile to the same target language, and so once we have compilers, and concurrent with the verification effort, you will experiment building small programs that use a mixture of different student languages.</p>
<h3 id="a-note-on-collaboration">A note on collaboration</h3>
<p>This will be a highly collaborative course. For the first section, the actual assignments will be done individually, to ensure that you get sufficient practice with theorem-proving, as proof assistants like Coq are not something you can learn without using. Even so, we <em>expect and encourage people to work together throughout the course</em>, provided that the actual work they submit is their own. Once the first section ends, the course will truly become a large collaboration. All of our compilers will be worked on in a shared repository, and while you will be assessed on and be responsible for understanding your own compiler, all are welcome to help any of their classmates. We will do also do group reviews or reviews of one group by another.</p>
<h3 id="requirements">Requirements</h3>
<p>Intended for advanced undergraduates, you would be well prepared by either having taken CS4400 (programming languages) or CS4410 (compilers). However, if you are interested and haven’t taken either, <strong>please reach out to the instructor</strong>. Additionally, familiarity with typed functional languages (e.g., Scala, Haskell, or OCaml) would be helpful, as would any exposure to formal proof in mathematics.</p>
<h3 id="other-question-something-not-clear">Other question? Something not clear?</h3>
<p>Please reach out to the instructor:</p>
<table>
<tbody>
<tr class="odd">
<td>Daniel Patterson</td>
</tr>
<tr class="even">
<td><a href="mailto:dbp@dbpmail.net">dbp@dbpmail.net</a></td>
</tr>
</tbody>
</table>
<p><br /><br /></p>

</body>
</html>
Binary file modified _site/static/resume.pdf
View file
Binary file not shown.
90 changes: 90 additions & 0 deletions courses/verifcomp.markdown
View file
@@ -0,0 +1,90 @@
---
title: "Verified Compilers and Multi-Language Software"
---

------- -------
Course CS4910: Verified Compilers and Multi-Language Software
Semester Fall 2019
Meeting Monday/Thursday, 11:45AM-1:25PM
Instructor Daniel Patterson ([dbp@dbpmail.net](mailto:dbp@dbpmail.net))
Office WVH 308
-------- ------

> “Can you trust your compiler?”
> &mdash; Xavier Leroy, developer of the Compcert verified C compiler

### Why this course?
Software is written in a variety of languages, and in many cases, in order to
run, it must be compiled down to some lower-level target. **But what if that
compiler isn't correct?** Compilers are some of the trickier pieces of software
we build, and yet bugs in them can be insidious, as bugs in compilers means that
one of our most basic debugging strategies, reading source code, may not be
helpful, since the source may have been miscompiled.

We want, essentially, the compiler to be invisible. But it can only truly be
invisible if we can be sure that it does exactly what we expect: if we have
proved it correct. Colliding with the field of verified compilation is the
question of how different languages should be able to interact -- that
interaction, or linking, happens after compilation, in the lower-level target
language. But the goal is to write source-level programs, not thinking about how
our various languages compile, and so again, we want the compiler to be
invisible.

These are our high-level motivations. The course itself, while motivated with
these problems, will be quite low-level: we will be **building languages,
compilers, and proving them correct**.

### How will the course be structured?
**Part 1.** We want to produce verified compilers, and so we will use one of the
state-of-the-art tools: the Coq proof assistant. This system allows us to write
functional programs and prove properties about them; afterwards we can extract
runnable versions of the verified programs. The first section of the course will
be dedicated to learning Coq and becoming familiar with the process of
_mechanized_ proof -- that is, proofs that are checked by a machine. The text
that we will use for this section of the course is ["Programs and Proofs" by
Ilya Sergey](https://ilyasergey.net/pnp).

**Part 2.** This part of the course will involve designing, in groups, different
source languages. These will all likely be simple functional languages, and we
will do plenty of design review to ensure that the language design you pick will
not cause too much difficulty later on.

**Part 3.** The final part will involve building and proving correct compilers
from your language to a common low-level target language. All the languages will
compile to the same target language, and so once we have compilers, and
concurrent with the verification effort, you will experiment building small
programs that use a mixture of different student languages.

### A note on collaboration
This will be a highly collaborative course. For the first section, the actual
assignments will be done individually, to ensure that you get sufficient
practice with theorem-proving, as proof assistants like Coq are not something
you can learn without using. Even so, we _expect and encourage people to work
together throughout the course_, provided that the actual work they submit is
their own. Once the first section ends, the course will truly become a large
collaboration. All of our compilers will be worked on in a shared repository,
and while you will be assessed on and be responsible for understanding your own
compiler, all are welcome to help any of their classmates. We will do also do
group reviews or reviews of one group by another.


### Requirements
Intended for advanced undergraduates, you would be well prepared by either
having taken CS4400 (programming languages) or CS4410 (compilers). However, if
you are interested and haven't taken either, **please reach out to the instructor**.
Additionally, familiarity with typed functional languages (e.g., Scala, Haskell,
or OCaml) would be helpful, as would any exposure to formal proof in
mathematics.


### Other question? Something not clear?

Please reach out to the instructor:

---------
Daniel Patterson
[dbp@dbpmail.net](mailto:dbp@dbpmail.net)
---------

<br/><br/>
12 changes: 12 additions & 0 deletions site
View file
Expand Up @@ -7,9 +7,12 @@ import Control.Category (id)
import Control.Monad (forM_)
import qualified Data.ByteString.Lazy as LBS
import Data.Monoid (mappend, mconcat, mempty, (<>))
import qualified Data.Set as Set
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
import Prelude hiding (id)
import Text.Pandoc.Options (Extension (Ext_simple_tables),
readerExtensions)

import Hakyll

Expand All @@ -30,6 +33,8 @@ gzip = withItemBody
. TE.encodeUtf8
. T.pack)

pandoc = pandocCompilerWith defaultHakyllReaderOptions {readerExtensions = Set.singleton Ext_simple_tables} defaultHakyllWriterOptions

main :: IO ()
main = hakyllWith config $ do
-- Compress CSS
Expand Down Expand Up @@ -77,6 +82,12 @@ main = hakyllWith config $ do
>>= loadAndApplyTemplate "templates/default.html" essayCtx
>>= relativizeUrls

match "courses/*.markdown" $ do
route (customRoute $ \ident -> let url = reverse (drop (length (".markdown" :: String)) (reverse (toFilePath ident))) in
url <> "/index.html")
compile $ pandocCompiler
>>= loadAndApplyTemplate "templates/course.html" defaultContext
>>= relativizeUrls

-- Render essays list
create ["essays.html"] $ do
Expand All @@ -89,6 +100,7 @@ main = hakyllWith config $ do
>>= loadAndApplyTemplate "templates/default.html" ctx
>>= relativizeUrls


-- Render static pages
match "index.markdown" $ do
route $ setExtension ".html"
Expand Down
Binary file modified static/resume.pdf
View file
Binary file not shown.
17 changes: 17 additions & 0 deletions templates/course.html
View file
@@ -0,0 +1,17 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>dbp.io :: $title$</title>
<link rel="stylesheet" type="text/css" href="/css/default.css" />
<link rel="stylesheet" type="text/css" href="/css/syntax.css" />
</head>
<body>

<h2>$title$</h2>

$body$

</body>
</html>

0 comments on commit c677167

Please sign in to comment.