• Vellvm

  • Referenced in 6 articles [sw13286]
  • mechanized formal semantics of LLVM’s intermediate representation, its type system, and properties ... framework is built using the Coq interactive theorem prover. It includes multiple operational semantics...
  • Ivor

  • Referenced in 3 articles [sw06343]
  • used to embed theorem proving technology in an implementation of a simple functional programming language ... using type theory as a core representation, we can construct and evaluate terms and prove ... ensuring consistency of the implementation and the theorem prover...
  • Psi-calculi

  • Referenced in 11 articles [sw28573]
  • have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package ... have been proposed over the last decades, representations for such binding sequences are not very...
  • FEMorph

  • Referenced in 5 articles [sw36217]
  • automatically generate both the classical boundary representation and the weak or “volume” formulation of first ... tool can either automatically apply the divergence theorem in tangent spaces for the strong form...
  • MahonianStat

  • Referenced in 12 articles [sw06180]
  • known (see, e.g., {[it P. Diaconis}, Group representations in probability and statistics, IMS Lecture Notes ... study of a local limit theorem to accompany our central limit theorem. Here our result...
  • BAT

  • Referenced in 7 articles [sw00067]
  • validity of a model as a representation of the data, and to extract the values ... Bayesian inference. BAT is based on Bayes’ Theorem and is realized with...
  • ARA

  • Referenced in 5 articles [sw08504]
  • relation algebras. ARA is an automatic theorem prover for various kinds of relation algebras ... semi-associative relation algebras, relation algebras and representable relation algebras using the calculi...
  • Gmeta

  • Referenced in 4 articles [sw10110]
  • generic libraries of infrastructure for first-order representations such as locally nameless or de Bruijn ... generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMeta’s modular...
  • Groebner_Bases

  • Referenced in 3 articles [sw32224]
  • statement and proof of the main theorem of the theory, the formalization also implements Buchberger ... functions can be executed on a concrete representation of multivariate polynomials as association lists...
  • Gauss-Jordan

  • Referenced in 3 articles [sw28564]
  • formalization is based on the Rank Nullity Theorem entry ... code generator to make this representation executable. In order to improve the performance, a refinement...
  • SAGEMoLiC

  • Referenced in 1 article [sw29863]
  • equivalence relations between machine models and/or language representations of formal languages by means ... previous systems, our approach to visualize equivalence theorems is not a simple “step by step ... conversion algorithms between computational models and/or grammatical representations of formal languages, because we make emphasis...
  • FourierMotzkin

  • Referenced in 2 articles [sw27120]
  • finite set of vectors. The fundamental theorem for cones states that a convex cone ... Motzkin) for converting between these two basic representations for convex cones. For polytopes, this allows...
  • Dubins explorer

  • Referenced in 3 articles [sw16416]
  • homotopy classes of bounded curvature paths. Graphical representations of data as heat maps are incorporated ... implementing a constructive proof of Dubins´ theorem in homotopy classes on flat surfaces...
  • Panoptes

  • Referenced in 1 article [sw09139]
  • assistants aid the user in proving mathematical theorems by taking care of low-level reasoning ... tool that enables users to explore graphical representations of the formal proofs produced...
  • Unbound

  • Referenced in 4 articles [sw22613]
  • Binders unbound. mplementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that ... this language derived from a locally nameless representation and prove that it satisfies a number...
  • UnstableManifoldCompactMap

  • Referenced in 1 article [sw22780]
  • truncation our goal is to obtain a representation of the invariant manifold which is accurate ... arithmetic), leads to mathematically rigorous computer assisted theorems describing precisely the truncation errors...
  • BEMLIB

  • Referenced in 101 articles [sw00005]
  • BEMLIB is a boundary-element software library of...
  • ANSYS

  • Referenced in 655 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...