
CoLoR
 Referenced in 38 articles
[sw09806]
 Turingcomplete formalism of term rewriting. Over the years, many methods and tools have been ... address the problem of deciding termination for specific problems (since it is undecidable in general ... formalising important results of the theory of wellfounded (rewrite) relations in the proof assistant...

iJulienne
 Referenced in 6 articles
[sw09903]
 specifications with iJulienne. We present iJulienne, a trace analyzer for conditional rewriting logic theories that...

ChC 3
 Referenced in 11 articles
[sw09781]
 ordersorted rewrite theories. For a rewrite theory to be executable, its equations E should ... crucially depends on the theory being ground coherent. Furthermore, many specifications of interest are typed ... ground coherence checking for ordersorted rewrite theories under these general assumptions. We also explain...

NuprlLight
 Referenced in 1 article
[sw31982]
 NuprlLight also allows theories to contain specifications of rewrites, using the computational congruence...

Anima
 Referenced in 4 articles
[sw10101]
 trace content to be searched for specific components. This paper presents a rich and highly ... technique for the trace inspection of Rewriting Logic theories that allows the nondeterministic execution...

HERMIT
 Referenced in 3 articles
[sw09886]
 support writing generalpurpose transformations: a domainspecific language for strategic programming specialized ... core language, a library of primitive rewrites, and a shellstyle–based scripting language ... because the developers’ interest is in theory rather than implementation. The mechanization process can often...

DistOrc
 Referenced in 5 articles
[sw10063]
 with Formal Analysis. Orc is a theory of orchestration of services that allows structured programming ... have been proposed for Orc, including a rewriting logic semantics developed by the authors ... overcome problems (i) and (ii) for Orc. Specifically, we describe an implementation technique based...

PetriPDL
 Referenced in 3 articles
[sw15081]
 proving that they comply with their specification. Petri nets fulfill these requirements as a formal ... work presents a prototype implementation, in the Rewriting Logic language Maude, of a bounded model ... representation of Kripke models as rewrite theories defined for the Linear Temporal Logic model checker...

Stream Fusion Code
 Referenced in 1 article
[sw28590]
 fusible list functions in the theories List and Coinductive_List, and prove them correct with ... lazy lists to prove the GHC compiler rewrite rules correct. In contrast, this work enables ... Coinductive entry. The fusible list functions require specification and proof principles different from Huffman...

SQLCert
 Referenced in 1 article
[sw28676]
 theoretical foundations and the corresponding standard specification, as SQL history spread over decades. Briefly ... treatment of relations: finite sets in theory, finite bags in practice, the treatment of attributes ... compilers’ logical optimisation is based on algebraic rewritings, we also define ExtAlg a Coqmechanised...

ATLAS
 Referenced in 197 articles
[sw00056]
 This paper describes the Automatically Tuned Linear Algebra...

ACL2
 Referenced in 279 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1807 articles
[sw00161]
 Coq is a formal proof management system. It...

dpgb
 Referenced in 16 articles
[sw00217]
 Improving the DISPGB algorithm using the discriminant ideal...

GAP
 Referenced in 2876 articles
[sw00320]
 GAP is a system for computational discrete algebra...

HasCasl
 Referenced in 17 articles
[sw00399]
 HasCasl: integrated higherorder specification and program development...

Isabelle
 Referenced in 611 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Maple
 Referenced in 5124 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 5957 articles
[sw00554]
 Almost any workflow involves computing results, and that...

MiniSat
 Referenced in 536 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...