Skip to content

lgaeher/metacoq

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

MetaCoq

MetaCoq

Build Status MetaCoq Chat

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 dedicated folder.

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

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

  • Reification of the environment structures, for constant and inductive declarations.

  • Denotation of terms and global declarations

  • A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MTac.

A partial type-checker for the Calculus of Inductive Constructions, whose extraction to ML is runnable as a plugin (using command MetaCoq Check foo). This checker uses fuel, so it must be passed a number of maximal reduction steps to perform when calling conversion, and is NOT verified.

PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is a cleaned up version of the term language of Coq and its associated type system, 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 conversion and validity of typing.

  • Subject Reduction (case/cofix reduction excluded)

  • Principality: every typeable term has a smallest type.

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

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 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>

An erasure procedure to untyped lambda-calculus accomplishing the same as 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.

Examples of translations built on top of this:

Examples

Papers

Team & Credits

Abhishek Anand Danil Annenkov Simon Boulier
Cyril Cohen Yannick Forster Gregory Malecha
Matthieu Sozeau Nicolas Tabareau Théo Winterhalter

MetaCoq is developed by (left to right) Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.

Copyright (c) 2014-2020 Gregory Malecha
Copyright (c) 2015-2020 Abhishek Anand, Matthieu Sozeau
Copyright (c) 2017-2020 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 2018-2020 Danil Annenkov, Yannick Forster, Théo Winterhalter

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.

Packages

No packages published

Languages

  • Coq 96.1%
  • OCaml 3.4%
  • Other 0.5%