olaure01 / color Goto Github PK
View Code? Open in Web Editor NEWThis project forked from fblanqui/color
Coq library on rewriting theory and termination
Home Page: http://color.inria.fr/
License: Other
This project forked from fblanqui/color
Coq library on rewriting theory and termination
Home Page: http://color.inria.fr/
License: Other
This is the CoLoR library. Check http://color.inria.fr/ for more recent versions. CoLoR is a library for the Coq proof assistant/checker (http://coq.inria.fr/) providing definitions and theorems about the termination/well-foundedness of arbitrary relations and rewrite relations on various term structures. Among other things, it includes: * libraries on logic in the Util/ subdirectory: - Logic: meta-theorems, tactics, possible axioms * libraries on mathematical structures in the Util/ directory: - Set: (infinite) sets - Relation: (infinite) binary relations/graphs - Algebra: (ordered) semi-rings * libraries on data structures in the Util/ subdirectory: - Bool: booleans - Option: option type - Nat: natural numbers - Integer: integers - Pair: type of pairs - List: lists - Vector: vectors - FSet: finite sets - FMap: finite maps - Multiset: finite multisets - Polynom: integer polynomials with multiple variables - Matrix: matrices over an (ordered) semi-ring - FGraph: finite graphs * libraries on term structures in the Term/ subdirectory: - String: words - Varyadic: varyadic terms - WithArity: algebraic terms with symbols of fixed arity - SimpleType: simply typed lambda-terms with de Bruijn indices - Lambda: lambda-terms with explicit alpha-equivalence * transformation techniques: - Conversion: conversions between term structures - DP: dependency pairs transformation and graph decomposition - Filter: arguments filterings - SemLab: semantic labeling * (non-)termination criteria: - MannaNess: inclusion in some reduction ordering - PolyInt: polynomial interpretations - MatrixInt: matrix interpretations - MPO: multiset path ordering - RPO: recursive path ordering - HORPO: higher-order recursive path ordering - NonTermin: loop certification - SubtermCrit: subterm criterion (unfinished) - Term/Lambda: computability closure Contributions to this project are very welcome! LICENSE: this file describes the license governing this library. COPYRIGHTS: this file describes the copyrights holders. INSTALL: this file describes a compilation procedure. THANKS: thanks to various people for their comments or help. CHANGES: this file briefly describes the main changes between two releases. The development version is available on https://github.com/fblanqui/color . The following scripts provide some statistics: - coq_stat [<directory>] (default is .): provides the number of definitions, lemmas, etc. - color_stat: provides the number of Coq lines (including newlines and comments) for the various kinds of formalizations (mathematical structures, data structures, etc.) The directory Coccinelle is not part of CoLoR. It contains an adaptation of the Coccinelle library which is used in Conversion/Coccinelle.v. See Coccinelle/README for more information.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.