ASignature.mkSignature ar beq_symb_ok Definition Fs : list Sig := M.zero::M.succ::M.quot::M.minus::nil. Lemma Fs_ok : forall f : Sig, In f Fs. Proof. list_ok. Qed. Definition some_symbol : Sig := M.minus ,
Sig M.minus (Vcons (@Var S1 ,
Definition trsInt (f : S1.Sig) := match f as f return poly (@ASignature.arity sig f) with | M, => (0%Z, Vnil) :: nil | ... end ,
Constructions, Inductive Types and Strong Normalization, 1993. ,
Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000. ,
DOI : 10.1016/S0304-3975(99)00207-8
Fix-Point Equations for Well-Founded Recursion in Type Theory, Proc. of TPHOL'00 ,
DOI : 10.1007/3-540-44659-1_1
Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997. ,
DOI : 10.1017/S095679689700289X
Lambda Calculi with types, Handbook of logic in computer science, 1992. ,
DOI : 10.1017/cbo9781139032636
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Proc. of FLOPS'06 ,
DOI : 10.1007/11737414_9
URL : https://hal.archives-ouvertes.fr/inria-00564237
Executing Higher Order Logic, Proc. of TYPES'02 ,
DOI : 10.1007/3-540-45842-5_2
Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Higher-order dependency pairs, Proc. of WST'06 ,
URL : https://hal.archives-ouvertes.fr/inria-00084821
Definitions by rewriting in the Calculus of Constructions, MSCS, vol.15, issue.1, pp.37-92, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00105648
Computability Closure: Ten Years Later. Rewriting, Computation and Proof ? Essays Dedicated to J.-P. Jouannaud on the Occasion of His 60th Birthday, LNCS, vol.4600, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00161092
Automated verification of termination certificates, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-00763495
CoLoR: a Coq Library on Rewriting and termination, Proc. of WST'06 ,
URL : https://hal.archives-ouvertes.fr/inria-00084835
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures ,
DOI : 10.1007/978-0-387-09680-3_24
URL : https://hal.archives-ouvertes.fr/inria-00275382
Dedukti version 1.1.3, 2000. ,
An Efficient Coq Tactic for Deciding Kleene Algebras, Proc. of ITP'10 ,
DOI : 10.1007/978-3-642-14052-5_13
Theory and Tool Support for the Formal Verification of Cryptographic Protocols, 2008. ,
Finding Lexicographic Orders for Termination Proofs in Isabelle Certification Problem Format. 2010. Certification Problem Format, Proc. of TPHOL'07 ,
Modular Development of Certified Program Verifiers with a Proof Assistant, Proc. of ICFP'06 ,
Implementation of Modules in the Coq System, Proc. of TPHOL'03 ,
Maude Manual (Version 2.2), 2005. ,
Modelling permutations in Coq for Coccinelle. Rewriting, Computation and Proof ? Essays Dedicated to J.-P. Jouannaud for His 60th Birthday, LNCS, vol.4600, 2007. ,
Certification of Automated Termination Proofs, Proc. of FROCOS'07 ,
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125312
Mechanically Proving Termination Using Polynomial Interpretations, Journal of Automated Reasoning, vol.12, issue.1, pp.325-363, 2005. ,
DOI : 10.1007/s10817-005-9022-x
URL : https://hal.archives-ouvertes.fr/inria-00001167
Pattern Matching with Dependent Types, Proc. of TYPES'92 ,
Inductively defined types, Proc. of COLOG'88 ,
DOI : 10.1007/3-540-52335-9_47
An effective proof of the well-foundedness of the multiset path ordering, Applicable Algebra in Engineering, Communication and Computing, vol.43, issue.2, pp.453-469, 2006. ,
DOI : 10.1007/s00200-006-0020-y
Certifying a Termination Criterion Based on Graphs, without Graphs, Proc. of TPHOL'08 ,
DOI : 10.1007/10704567_3
URL : https://hal.archives-ouvertes.fr/hal-01125530
A Tactic Language for the System Coq, Proc. of LPAR'00, 1955. ,
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070
Termination by Abstraction, Proc. of ICLP'04 ,
DOI : 10.1007/978-3-540-27775-0_1
Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982. ,
DOI : 10.1016/0304-3975(82)90026-3
Rewrite Systems, Handbook of Theoretical Computer Science, 1990. ,
DOI : 10.1016/B978-0-444-88074-1.50011-1
Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003. ,
DOI : 10.1007/BFb0037116
Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003. ,
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proc. of IJCAR'06 ,
DOI : 10.1007/11814771_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.2217
Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages, RTA'06 ,
DOI : 10.1007/11805618_23
Improving Dependency Pairs, Proc. of LPAR'03 ,
DOI : 10.1007/978-3-540-39813-4_11
Modular Termination Proofs for Rewriting Using Dependency Pairs, Journal of Symbolic Computation, vol.34, issue.1, pp.21-58, 2002. ,
DOI : 10.1006/jsco.2002.0541
Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006. ,
DOI : 10.1007/s10817-006-9057-7
Codifying Guarded Definitions with Recursion Schemes, TYPES'94 ,
Proofs and Types, 1988. ,
A Small Scale Reflection extension for the Coq system, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
A compiled implementation of strong reduction, Proc. of ICFP'02 ,
Code Generation via Higher-Order Rewrite Systems, Proc. of FLOPS'10 ,
DOI : 10.1007/978-3-642-12251-4_9
Certification des preuves de terminaison par interprétations polynomiales, 2004. ,
Automating the Dependency Pair Method, IC, vol.199, issue.12, pp.172-199, 2005. ,
Tyrolean termination tool: Techniques and features, Information and Computation, vol.205, issue.4, pp.474-511, 2007. ,
DOI : 10.1016/j.ic.2006.08.010
Automated Complexity Analysis Based on the Dependency Pair Method, Proc. of IJCAR'08 ,
DOI : 10.1007/978-3-540-71070-7_32
Heq: A Coq library for Heterogeneous Equality, 2009. ,
The Higher-Order Recursive Path Ordering Simple word problems in universal algebra. Computational problems in abstract algebra, Proc. of LICS'99, 1967. ,
Certified Higher-Order Recursive Path Ordering, Proc. of RTA'06 ,
DOI : 10.1007/11805618_17
Termination of rewriting and its certification, 2008. ,
Coq formalization of the higher-order recursive path ordering, Applicable Algebra in Engineering, Communication and Computing, vol.32, issue.2, pp.5-6, 2009. ,
DOI : 10.1007/s00200-009-0105-5
Certification of Proving Termination of Term Rewriting by Matrix Interpretations, Proc. of SOFSEM'08 ,
DOI : 10.1007/978-3-540-77566-9_28
Tyrolean Termination Tool 2, Proc. of RTA'09 ,
DOI : 10.1007/978-3-540-70590-1_23
Certified Size-Change Termination, Proc. of CADE'07 ,
DOI : 10.1007/978-3-540-73595-3_34
Argument Filtering Transformation, Proc. of PPDP'99 ,
DOI : 10.1007/10704567_3
On Proving term rewriting systems are Noetherian, 1979. ,
The Objective Caml system release 3.12, Documentation and user's manual, 2010. ,
A New Extraction for Coq, Proc. of TYPES'02 ,
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914
On the termination of Markov algorithms, Proc. of HICSS'70 ,
Analysing the implicit complexity of programs, Information and Computation, vol.183, issue.1, pp.2-18, 2003. ,
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00099505
Dependently typed functional programs and their proofs, 1999. ,
Termination Analysis of Logic Programs Based on Dependency Graphs, Proc. of LOPSTR'07 ,
DOI : 10.1007/s00200-005-0179-7
Extracting F?'s Programs from Proofs in the Calculus of Constructions, Proc. of POPL'89 ,
Inductive definitions in the system Coq rules and properties, Proc. of TLCA'93 ,
DOI : 10.1007/BFb0037116
Haskell 98 Language and Libraries, The revised report, 2003. ,
Typing algorithm in type theory with inheritance, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97 ,
DOI : 10.1145/263699.263742
Proving Termination Using Recursive Path Orders and SAT Solving, Proc. of FROCOS'07 ,
DOI : 10.1007/978-3-540-74621-8_18
Automated termination proofs for logic programs by term rewriting, ACM Transactions on Computational Logic, vol.11, issue.1, pp.1-52, 2009. ,
DOI : 10.1145/1614431.1614433
First-Class Type Classes, Proc. of TPHOL'08 ,
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864
PROGRAM-ing Finger trees in Coq, Proc. of ICFP'07 ,
Root-Labeling, Proc. of RTA'08 ,
DOI : 10.1007/978-3-540-70590-1_23
Certification of Termination Proofs using CeTA, Proc. of TPHOL'09 ,
Certified Subterm Criterion and Certified Usable Rules, Proc. of RTA'10 ,
Investigations into Intensional Type Theory, 1993. ,
Coq Modulo Theory, Proc. of CSL'10 ,
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404
Coq modulo theories Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science Termination Portal. http://termination-portal.org/ Termination Problem Data Base (TPDB) http://termination-portal.org/wiki/TPDB Waldmann, Proc. of WST'09 Consistency and completeness of rewriting in the Calculus of Constructions, pp.1-20, 2003. ,
Une Théorie des Constructions Inductives, 1994. ,
Termination of Term Rewriting by Semantic Labelling, Fundamenta Informaticae, vol.24, pp.89-105, 1995. ,