Git Product home page Git Product logo

certicoq's Introduction

CertiCoq

CertiCoqCoq

Overview

CertiCoq is a compiler for Gallina, the specification language of the Coq proof assistant. CertiCoq targets Clight, a subset of the C language that can be compiled with any C compiler, including the CompCert verified compiler.

Large parts of the CertiCoq compiler have been verified whereas others are in the process of being verified.

Documentation

The CertiCoq Wiki has instructions for using the CertiCoq plugin to compile Gallina to C and interfacing with the generated C code.

You can also find some demos here and here.

Installation Instructions

See INSTALL.md for installation instructions.

Current Members

Andrew Appel, Yannick Forster, Anvay Grover, Joomy Korkut, John Li, Zoe Paraskevopoulou, and Matthieu Sozeau.

Past Members and Contributors

Abhishek Anand, Greg Morrisett, Randy Pollack, Olivier Savary Belanger, Matthew Weaver

License

CertiCoq is open source and distributed under the MIT license.

Directory structure

  • theories/ contains the sources of the compiler
  • plugin/ contains the CertiCoq plugin for Coq
  • benchmarks/ contains the benchmark suite
  • glue/ contains the glue code generator

Structure of the theories directory:

  • theories/common: contains common code utilities
  • theories/Compiler: contains the toplevel CertiCoq pipeline
  • theories/L1g: 1st pass, moves from (MetaCoq's) λbox to our similar L1g
  • theories/L2k_noCnstrParams: 2nd pass, eta expands constructors and removes constructor parameters
  • theories/L4_deBruijn: 3rd pass, let-bind environment
  • theories/L6_PCPS contains the λANF pipeline (and conversions -- direct and CPS -- to λANF)
  • theories/L7 contains the C code generator.
  • theories/compcert contains a local copy of the compcert compiler

Bugs

We use github's issue tracker to keep track of bugs and feature requests.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.