We stand with Ukraine to help keep people safe. Join us
All Apps
Best AppsReviewsComparisonsHow-To
Coq free download for Mac

Coq

Version 8.16.1

Formal proof management system for mathematics.

3.5
Based on 1 user rateRead reviews & comments
Free
Absolutely Free

Coq overview

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

What’s new in version 8.16.1

Updated on Mar 06 2023

Summary of changes

Coq version 8.16 integrates changes to the Coq kernel and performance improvements along with a few new features. We highlight some of the most impactful changes here:

  • The guard checker (see Guarded) now ensures strong normalization under any reduction strategy.
  • Irrelevant terms (in the SProp sort) are now squashed to a dummy value during conversion, fixing a subject reduction issue and making proof conversion faster.
  • Introduction of reversible coercions, which allow coercions relying on meta-level resolution such as type-classes or canonical structures. Also allow coercions that do not fullfill the uniform inheritance condition.
  • Generalized rewriting support for rewriting with Type-valued relations and in Type contexts, using the Classes.CMorphisms library.
  • Added the boolean equality scheme command for decidable inductive types.
  • Added a Print Notation command.
  • Incompatibilities in name generation for Program obligations, eauto treatment of tactic failure levels, use of ident in notations, parsing of module expressions.
  • Standard library reorganization and deprecations.
  • Improve the treatment of standard library numbers by Extraction.

Information

License

Free

Size

854.2 MB

Developer’s website

https://coq.inria.fr

Downloads

3094

App requirements

Try our new feature and write a detailed review about Coq. All reviews will be posted soon.

Write your thoughts in our old-fashioned comment

MacUpdate Comment Policy. We strongly recommend leaving comments, however comments with abusive words, bullying, personal attacks of any type will be moderated.
0.0

(0 Reviews of )

There are no reviews yet
  • Comments

  • User Ratings

Guest
Guest
May 3 2004
8.0
3.5
May 3 2004
3.5
Version: 8.0
Packagers need to spend some time (re-)learning UNIX best practices. Installing directly into /usr (instead of /usr/local) is bad form.
Guest
Guest
May 1 2004
8.0
3.5
May 1 2004
3.5
Version: 8.0
I can't get coq to work.
Guest
Guest
May 1 2004
8.0
3.5
May 1 2004
3.5
Version: 8.0
Coq rulez !
Guest
Guest
May 1 2004
3.5
May 1 2004
3.5
Version: null
Free
Absolutely Free
How would you rate Coq?
Similar apps
Mathematica
Advanced mathematics, visualization, and more.
Is this app is similar to Mathematica? Vote to improve the quality of this list.
Vote results
1
Upvotes
1
Total score
0
Downvotes
Eigenmath
Symbolic math program.
Is this app is similar to Eigenmath? Vote to improve the quality of this list.
Vote results
1
Upvotes
1
Total score
0
Downvotes
MathBoard
Learn math the fun and easy way.
Is this app is similar to MathBoard? Vote to improve the quality of this list.
Vote results
1
Upvotes
1
Total score
0
Downvotes