Skip to content

vfa-current

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History
 
 

vfa-current

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
.devcontainer
.devcontainer
 
 
common
common
 
 
ADT.html
ADT.html
 
 
ADT.v
ADT.v
 
 
ADTTest.v
ADTTest.v
 
 
BagPerm.html
BagPerm.html
 
 
BagPerm.v
BagPerm.v
 
 
BagPermTest.v
BagPermTest.v
 
 
Binom.html
Binom.html
 
 
Binom.v
Binom.v
 
 
BinomTest.v
BinomTest.v
 
 
Color.html
Color.html
 
 
Color.v
Color.v
 
 
ColorTest.v
ColorTest.v
 
 
Decide.html
Decide.html
 
 
Decide.v
Decide.v
 
 
DecideTest.v
DecideTest.v
 
 
Extract.html
Extract.html
 
 
Extract.v
Extract.v
 
 
ExtractTest.v
ExtractTest.v
 
 
LICENSE
LICENSE
 
 
Makefile
Makefile
 
 
Maps.html
Maps.html
 
 
Maps.v
Maps.v
 
 
MapsTest.v
MapsTest.v
 
 
Merge.html
Merge.html
 
 
Merge.v
Merge.v
 
 
MergeTest.v
MergeTest.v
 
 
Multiset.html
Multiset.html
 
 
Multiset.v
Multiset.v
 
 
MultisetTest.v
MultisetTest.v
 
 
Perm.html
Perm.html
 
 
Perm.v
Perm.v
 
 
PermTest.v
PermTest.v
 
 
Preface.html
Preface.html
 
 
Preface.v
Preface.v
 
 
PrefaceTest.v
PrefaceTest.v
 
 
Priqueue.html
Priqueue.html
 
 
Priqueue.v
Priqueue.v
 
 
PriqueueTest.v
PriqueueTest.v
 
 
README
README
 
 
Redblack.html
Redblack.html
 
 
Redblack.v
Redblack.v
 
 
RedblackTest.v
RedblackTest.v
 
 
SearchTree.html
SearchTree.html
 
 
SearchTree.v
SearchTree.v
 
 
SearchTreeTest.v
SearchTreeTest.v
 
 
Selection.html
Selection.html
 
 
Selection.v
Selection.v
 
 
SelectionTest.v
SelectionTest.v
 
 
Sort.html
Sort.html
 
 
Sort.v
Sort.v
 
 
SortTest.v
SortTest.v
 
 
Trie.html
Trie.html
 
 
Trie.v
Trie.v
 
 
TrieTest.v
TrieTest.v
 
 
_CoqProject
_CoqProject
 
 
coqindex.html
coqindex.html
 
 
deps.html
deps.html
 
 
deps.svg
deps.svg
 
 
index.html
index.html
 
 
redblack.ml
redblack.ml
 
 
redblack.mli
redblack.mli
 
 
searchtree.ml
searchtree.ml
 
 
searchtree.mli
searchtree.mli
 
 
test_searchtree.ml
test_searchtree.ml
 
 
toc.html
toc.html
 
 
vfa.tgz
vfa.tgz
 
 

README

#########################################################################
                           SOFTWARE FOUNDATIONS
#########################################################################

This directory contains both Coq scripts (.v files) and more readable
HTML files for Verified Functional Algorithms, by Andrew W. Appel,
volume 3 of the Software Foundations series.

  - VFA.v or VFA.html
    The place to start reading, including details on how to install
    required software

  - index.html
    The book's cover page and navigation starting point

  - deps.html
    Overview of the ordering of chapters

  - LICENSE
    Explanation of how these files may be redistributed