A Formalisation (in Coq) of Nominal C-Unification and Nominal A, C and AC-Equivalence
The current version of this dataset is also available at https://doi.org/10.5281/zenodo.3364517.
Compiled with the Coq Proof Assistant Version 8.7.2:
| File/Folder | Short description |
|---|---|
| thesis20190319.pdf | The text of the doctoral thesis entitled "Nominal Equational Problems Modulo Associativity, Commutativity and Associativity-Commutativity" |
| Impl_Equiv/ | Folder with the implementations of the naive (extracted from the specification) and of the improved nominal A, C and AC-checking algorithms (OCaml code) |
| Impl_Unif/ | Folder with the implementation of the nominal C-unification algorithm (OCaml code) |
| LibTactics.v | Library of tactics given by http://www.chargueraud.org/softs/tlc/ |
| Basics.v | Necessary basic results on arithmetics and lists that are not in the standard libraries of Coq |
| Terms.v | Syntax definition of nominal terms and some properties about |
| Perm.v | Permutation action definition and its properties |
| Disgr.v | Disagreement set definition and its properties |
| Tuples.v | Definitions of TPlength, TPith and TPithdel and many formalised properties about |
| Fresh.v | Deftinition of the freshness relation and some related basic properties |
| Alpha_Equiv.v | Definition of the nominal alpha_equivalence and the formalisation of its soundness |
| Equiv.v | Extentions of nominal alpha_equivalence in a parametrised way |
| AACC_Equiv_rec | Recursive versions of the inductive definitions fresh and equiv from files Fresh.v and Equiv.v and OCaml code extraction |
| Equiv_Tuples.v | Interactions between the extentions of nominal alpha_equivalence and tuples |
| AACC_Equiv.v | Definitions of the nominal A+AC+C, A, AC and C-equivalences and the formalisation of their soundness |
| C_Equiv.v | Specific Lemmas about nominal C-equivalence |
| Problems.v | Definition of nominal C-unification problems and some lemmas about |
| Substs.v | Definition of substitutions and some lemmas about |
| C_Unif.v | Definition of the rule transformation systems |
| C_Unif_Termination.v | Formalisation of the termination of |
| C_Unif_Soundness.v | Formalisation of the soundness of |
| C_Unif_Completeness.v | Formalisation of the completeness of |
| C_Matching | Specification and formalisation of the properties of termination, soundness and completeness of the C-matching algorithm |
| Makefile | Organisation of the code compilation with the "make" tool |
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent