• CoLoR

  • Referenced in 38 articles [sw09806]
  • Turing-complete 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 well-founded (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]
  • order-sorted 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 order-sorted rewrite theories under these general assumptions. We also explain...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • Nuprl-Light 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 non-deterministic execution...
  • HERMIT

  • Referenced in 3 articles [sw09886]
  • support writing general-purpose transformations: a domain-specific language for strategic programming specialized ... core language, a library of primitive rewrites, and a shell-style–based scripting language ... because the developers’ interest is in theory rather than implementation. The mechanization process can often...
  • Dist-Orc

  • 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...
  • Petri-PDL

  • 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 Coq-mechanised...
  • 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 higher-order 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 SAT-solver. MiniSat is a minimalistic...