20
I Use This!
Very High Activity

News

Analyzed about 20 hours ago. based on code collected about 21 hours ago.
Posted over 11 years ago by letouzey
As part of the ADT Coq-API, we are now offering a 2-year position for a specialized engineer. For more details, see http://www.pps.univ-paris-diderot.fr/~letouzey/coq-api-position.html
Posted over 11 years ago by boutillier
Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the CHANGES file. WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.
Posted over 11 years ago by boutillier
Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the CHANGES file. WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.
Posted over 11 years ago by boutillier
Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the CHANGES file. WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.
Posted over 11 years ago by herbelin
After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award. The recipients of the award are thanking all developers who contributed to the success of Coq, the users who illustrated how to use Coq ... [More] for so many impressive projects in formal certification, programming, logic, formalization of mathematics and teaching as well as the whole surrounding scientific community in proof theory, type theory, programming languages, interactive theorem proving. All over 30 years, Coq also benefited from the trust and support from Inria and from its partners, CNRS, ENS Lyon, University Paris-Sud, École Polytechnique, University Paris-Diderot. [Less]
Posted over 11 years ago by herbelin
After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award. The recipients of the award are thanking all developers who contributed to the success of Coq, the users who illustrated how to use Coq ... [More] for so many impressive projects in formal certification, programming, logic, formalization of mathematics and teaching as well as the whole surrounding scientific community in proof theory, type theory, programming languages, interactive theorem proving. All over 30 years, Coq also benefited from the trust and support from Inria and from its partners, CNRS, ENS Lyon, University Paris-Sud, École Polytechnique, University Paris-Diderot. [Less]
Posted over 11 years ago by herbelin
After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award. read more
Posted about 12 years ago by letouzey
The main source repository for Coq on gforge.inria.fr is now using git instead of subversion. For accessing this new repository, see the "sources" page of the coq project on gforge. More details could be found on the wiki page about this transition. Happy git cloning :-)
Posted about 12 years ago by letouzey
The main source repository for Coq on gforge.inria.fr is now using git instead of subversion. For accessing this new repository, see the "sources" page of the coq project on gforge. More details could be found on the wiki page about this transition. Happy git cloning :-)
Posted about 12 years ago by letouzey
The main source repository for Coq on gforge.inria.fr is now using git instead of subversion. For accessing this new repository, see the "sources" page of the coq project on gforge. More details could be found on the wiki page about this transition. Happy git cloning :-)