Verified Coq Implementation of the Perceptron Algorithm
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Benchmarks
LICENSE
MCEBounds.v
Makefile
PerceptronConvergence.v
PerceptronDef.v
PerceptronSound.v
QvecArith.v
README.md
TerminationRefinement.v
_CoqProject
extraction.v

README.md

CoqPerceptron

Verified Coq Implementation of the Rational-Valued Perceptron Algorithm and Rational-Valued Averaged-Perceptron Algorithm.

Key Files

Coq

Benchmarks/

  • cpp/: C++ implementation of Perceptron; also, program to generate random data sets
  • hs/:Extracted CoqPerceptron to Haskell
  • hsopt/: Soundly Optimized Extraction of CoqPercepton to Haskell
  • data/: Real-world and randomly-generated data sets
  • output/:Output and timing results from running the CPP, HS, and HSOpt verions of the Perceptron.
  • scripts/: Scripts for generated random data sets and running benchmarks

Building the Coq Development

Simply type

make

Prerequisites

For building CoqPerceptron and C++ Perceptron Implementations

  • Coq 8.5pl2
  • GHC 7.6.3
  • G++ 4.8.4
  • Boost 1.54

For creating the plotting files

  • Python 2.7.6
  • matplotlib 1.3.1
  • gnuplot 4.6.4

Our development may compile with other versions, but this hasn't been tested.

Building CoqPerceptron (Benchmarks/hs/)

  cd Benchmarks/hs
  make

Building Optimized CoqPerceptron (Benchmarks/hsopt)

  cd Benchmarks/hsopt
  make

Building C++ Perceptron Implementation (Benchmarks/cpp)

  cd Benchmarks/cpp
  make

Running Benchmarks

Generating new DataSets

Note: This will overwrite the data in data/

  cd Benchmarks
  scripts/gen_data.sh

Run each Perceptron implementation on the generated data

  scripts/runbenchmarks.sh cpp/perceptron data/ output/cpp output/fuels hs/RunValidator output/cpp_valid.dat > output/cpptimes 2> output/cpp_validtimes
  scripts/runbenchmarks.sh hs/RunPerceptron data/ output/hs > output/hstimes
  scripts/runbenchmarks.sh hsopt/RunPerceptron data/ output/hsopt > output/hsopttimes

Note: You may wish to put this in a script and run that as each command may take a considerable amount of time to run

Creating Plot Files

  cpp/makeplotfiles
  cd plots
  python makeplots.py
  gnuplot epochs.gplot