frap/index.html

<html>
<head>
<link rel="stylesheet" type="text/css" href="/style.css">
<title>Formal Reasoning About Programs</title>
</head><body>
<h1>Formal Reasoning About Programs</h1>
<h2><a href="http://adam.chlipala.net/">Adam Chlipala</a></h2>

<div class="summary" style="overflow: hidden">

<p>This is the web site for the early stages of a book introducing both machine-checked proof with <a href="http://coq.inria.fr/">the Coq proof assistant</a> and approaches to formal reasoning about program correctness.</p>

<h2>Grab a Draft</h2>
<ul>
  <li><a href="https://github.com/achlipala/frap">Source on GitHub</a></li>
  <li><a href="frap_book.pdf">Quasi-latest PDF draft</a></li>
  <li><a href="frap.tgz">Quasi-latest source-code tarball</a></li>
  <li><a href="fraplib.tgz">Quasi-latest source-code tarball, library only</a> (warning: the author really does not recommend using it in serious projects!)</li>
</ul>
</div>

<div class="project">
<h2>Use in classes</h2>

<h3>Classes where FRAP is/was a primary text</h3>
<ul>
  <li>6.822 at MIT (<a href="https://frap.csail.mit.edu/">Spring 2022</a>, Spring 2021, Spring 2020, Spring 2018, Spring 2017 [as 6.887], Spring 2016 [as 6.887])</li>
  <ul>
    <li><a href="https://github.com/mit-frap/spring22">Spring 2022 exercises</a></li>
    <li><a href="https://github.com/mit-frap/spring21">Spring 2021 exercises</a></li>
    <li><a href="https://github.com/mit-frap/spring20">Spring 2020 exercises</a></li>
    <li><a href="https://github.com/mit-frap/spring18">Spring 2018 exercises</a></li>
    <li><a href="https://github.com/mit-frap/spring17">Spring 2017 exercises</a></li>
    <li><a href="https://github.com/mit-frap/spring16">Spring 2016 exercises</a></li>
  </ul>
  <li>EECS 755 at U. Kansas (<a href="http://perry.alexander.name/eecs755/">Spring 2020</a>)</li>
  <li>CS6225 at IIT Madras (<a href="http://kcsrk.info/cs6225_s20_iitm/">Spring 2020</a>)</li>
  <li>CSE 505 at U. Washington (<a href="https://sites.google.com/cs.washington.edu/cse-505-18au">Fall 2018</a>)</li>
</ul>

</div>

</body></html>
Publishing to web 2016-02-02 18:53:00 +00:00			`<html>`
			`<head>`
			`<link rel="stylesheet" type="text/css" href="/style.css">`
			`<title>Formal Reasoning About Programs</title>`
			`</head><body>`
			`<h1>Formal Reasoning About Programs</h1>`
			`<h2><a href="http://adam.chlipala.net/">Adam Chlipala</a></h2>`

			`<div class="summary" style="overflow: hidden">`

			`<p>This is the web site for the early stages of a book introducing both machine-checked proof with <a href="http://coq.inria.fr/">the Coq proof assistant</a> and approaches to formal reasoning about program correctness.</p>`

			`<h2>Grab a Draft</h2>`
			`<ul>`
			`<li><a href="https://github.com/achlipala/frap">Source on GitHub</a></li>`
Incorporating a variety of changes and pull requests, after things got desync'd a bit 2016-02-10 01:21:19 +00:00			`<li><a href="frap_book.pdf">Quasi-latest PDF draft</a></li>`
Publishing to web 2016-02-02 18:53:00 +00:00			`<li><a href="frap.tgz">Quasi-latest source-code tarball</a></li>`
Separate out library code with its own license 2020-03-17 13:22:06 +00:00			`<li><a href="fraplib.tgz">Quasi-latest source-code tarball, library only</a> (warning: the author really does not recommend using it in serious projects!)</li>`
Publishing to web 2016-02-02 18:53:00 +00:00			`</ul>`
			`</div>`

			`<div class="project">`
			`<h2>Use in classes</h2>`

Link to Spring 2020 users of the book 2020-02-08 15:46:47 +00:00			`<h3>Classes where FRAP is/was a primary text</h3>`
Publishing to web 2016-02-02 18:53:00 +00:00			`<ul>`
Latest MIT offering finished 2022-08-21 12:59:23 +00:00			`<li>6.822 at MIT (<a href="https://frap.csail.mit.edu/">Spring 2022</a>, Spring 2021, Spring 2020, Spring 2018, Spring 2017 [as 6.887], Spring 2016 [as 6.887])</li>`
Link to CSE 505 at UW 2018-10-27 12:22:04 +00:00			`<ul>`
Latest MIT offering finished 2022-08-21 12:59:23 +00:00			`<li><a href="https://github.com/mit-frap/spring22">Spring 2022 exercises</a></li>`
New semester 2021-02-17 13:47:42 +00:00			`<li><a href="https://github.com/mit-frap/spring21">Spring 2021 exercises</a></li>`
Link to Spring 2020 users of the book 2020-02-08 15:46:47 +00:00			`<li><a href="https://github.com/mit-frap/spring20">Spring 2020 exercises</a></li>`
Link to CSE 505 at UW 2018-10-27 12:22:04 +00:00			`<li><a href="https://github.com/mit-frap/spring18">Spring 2018 exercises</a></li>`
			`<li><a href="https://github.com/mit-frap/spring17">Spring 2017 exercises</a></li>`
			`<li><a href="https://github.com/mit-frap/spring16">Spring 2016 exercises</a></li>`
			`</ul>`
Link to Spring 2020 users of the book 2020-02-08 15:46:47 +00:00			`<li>EECS 755 at U. Kansas (<a href="http://perry.alexander.name/eecs755/">Spring 2020</a>)</li>`
			`<li>CS6225 at IIT Madras (<a href="http://kcsrk.info/cs6225_s20_iitm/">Spring 2020</a>)</li>`
			`<li>CSE 505 at U. Washington (<a href="https://sites.google.com/cs.washington.edu/cse-505-18au">Fall 2018</a>)</li>`
Publishing to web 2016-02-02 18:53:00 +00:00			`</ul>`

			`</div>`

			`</body></html>`