Skip to content

Latest commit

 

History

History
68 lines (49 loc) · 2.53 KB

resources.md

File metadata and controls

68 lines (49 loc) · 2.53 KB
Raw
layout title permalink
page
Resources
/resources/

Course Website

This course website, including all of the lecture materials, lives here.

Software

Coq

For Coq, I use CoqIDE. If you are an emacs user, then Proof General is recommended.

You will need to ensure that the location of the Coq binaries is in your PATH so that the make files for the frap book and the assignments work. On MacOS, this means that the following line is included in my .bashrc file:

export PATH=$PATH:/Applications/CoqIDE_8.10.2.app/Contents/Resources/bin/

This will vary between OS versions. We will ensure that everyone has a working environment by the end of first week.

F*

The easiest way to try out F* quickly is directly in your browser using the online editor that's part of the F* tutorial. There is also a better, experimental online editor.

I use Spacemacs + Fstar-mode.el + Spacemacs layer for F*. I recommend this setup for interactive development.

Text Books

We will be closely following

  • Formal Reasoning about Programs, Adam Chlipala. Freely available online.

for the Coq part of the course. For F*, there is no prescribed text book. We will look at examples from the tutorials and other lectures.

Other reference books are:

  • Software Foundations, Benjamin Pierce et al. Freely available online.
  • Types and Programming Languages, Benjamin Pierce, MIT Press, 1st edition, 2002. Ebook is available in IITM library.
  • Practical Foundations for Programming Languages, Robert Harper, Cambridge University Press, 2nd edition, 2016. Freely available online.

Tactics Reference