Giter Club home page Giter Club logo

metacoq's Introduction

MetaCoq

MetaCoq

Build status MetaCoq Chat Open in Visual Studio Code

MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.

Quick jump

Getting started

Installation instructions

See INSTALL.md

Documentation

See DOC.md

Overview of the project

At the center of this project is the Template-Coq quoting library for Coq. The project currently has a single repository extending Template-Coq with additional features. Each extension is in a dedicated folder. The dependency graph might be useful to navigate the project. Statistics: ~150kLoC of Coq, ~30kLoC of OCaml.

Template-Coq is a quoting library for Coq. It takes Coq terms and constructs a representation of their syntax tree as an inductive data type. The representation is based on the kernel's term representation.

After importing MetaCoq.Template.Loader there are commands MetaCoq Test Quote t., MetaCoq Quote Definition name := (t). and MetaCoq Quote Recursively Definition name := (t). as well as a tactic quote_term t k, where in all cases t is a term and k a continuation tactic.

In addition to this representation of terms, Template Coq includes:

  • Reification of the environment structures, for constant and inductive declarations along with their universe structures.

  • Denotation of terms and global declarations.

  • A monad for querying the environment, manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MTac. Monadic programs p : TemplateMonad A can be run using MetaCoq Run p.

  • A formalisation of the typing rules reflecting the ones of Coq, covering all of Coq except eta-expansion and template polymorphism.

PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is a cleaned up version of the term language of Coq and its associated type system, shown equivalent to the one of Coq. This version of the calculus has proofs of standard metatheoretical results:

  • Weakening for global declarations, weakening and substitution for local contexts.

  • Confluence of reduction using a notion of parallel reduction

  • Context cumulativity / conversion and validity of typing.

  • Subject Reduction (case/cofix reduction excluded)

  • Principality: every typeable term has a smallest type.

  • Bidirectional presentation: an equivalent presentation of the system that enforces directionality of the typing rules. Strengthening follows from this presentation.

  • Elimination restrictions: the elimination restrictions ensure that singleton elimination (from Prop to Type) is only allowed on singleton inductives in Prop.

  • Canonicity: The weak head normal form of a term of inductive type is a constructor application.

  • Consistency under the assumption of strong normalization

  • Weak call-by-value standardization: Normal forms of terms of first-order inductive type can be found via weak call-by-value evaluation.

See the PCUIC README for a detailed view of the development.

Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of strong normalization of the reduction relation of PCUIC on well-typed terms. The checker is shown to be correct and complete w.r.t. the PCUIC specification. The extracted safe checker is available in Coq through a new vernacular command:

MetaCoq SafeCheck <term>

After importing MetaCoq.SafeChecker.Loader.

To roughly compare the time used to check a definition with Coq's vanilla type-checker, one can use:

MetaCoq CoqCheck <term>

This also includes a verified, efficient re-typing procedure (useful in tactics) in MetaCoq.SafeChecker.PCUICSafeRetyping.

See the SafeChecker README for a detailed view of the development.

An erasure procedure to untyped lambda-calculus accomplishing the same as the type and proof erasure phase of the Extraction plugin of Coq. The extracted safe erasure is available in Coq through a new vernacular command:

MetaCoq Erase <term>

After importing MetaCoq.Erasure.Loader.

The erasure pipeline includes verified optimizations to remove lets in constructors, remove cases on propositional terms, switch to an unguarded fixpoint reduction rule and transform the higher-order constructor applications to first-order blocks for easier translation to usual programming languages. See the erasure README for a detailed view of the development.

Examples of translations built on top of this:

Examples

Papers

Team & Credits

Abhishek Anand Danil Annenkov Simon Boulier
Cyril Cohen Yannick Forster Meven Lennon-Bertrand
Kenji Maillard Gregory Malecha Jakob Botsch Nielsen
Matthieu Sozeau Nicolas Tabareau Théo Winterhalter

MetaCoq is developed by (left to right) Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Jakob Botsch Nielsen, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.

Copyright (c) 2014-2022 Gregory Malecha
Copyright (c) 2015-2022 Abhishek Anand, Matthieu Sozeau
Copyright (c) 2017-2022 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 2018-2022 Danil Annenkov, Yannick Forster, Théo Winterhalter
Copyright (c) 2020-2022 Jakob Botsch Nielsen, Meven Lennon-Bertrand
Copyright (c) 2022      Kenji Maillard

This software is distributed under the terms of the MIT license. See LICENSE for details.

Bugs

Please report any bugs or feature requests on the github issue tracker.

metacoq's People

Contributors

aa755 avatar annenkov avatar ejgallego avatar fakusb avatar flupe avatar gares avatar gasche avatar gmalecha avatar herbelin avatar jakobbotsch avatar jasongross avatar jfehrle avatar ju-sh avatar kyodralliam avatar mattam82 avatar maximedenes avatar mevenbertrand avatar namin avatar neuralcoder3 avatar palmskog avatar ppedrot avatar proux01 avatar simonboulier avatar skyskimmer avatar tabareau avatar theowinterhalter avatar vbgl avatar vzaliva avatar yannl35133 avatar yforster avatar

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.