
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...

Psicalculi
 Referenced in 11 articles
[sw28573]
 have formalised psicalculi 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 ... semiassociative relation algebras, relation algebras and representable relation algebras using the calculi...

Gmeta
 Referenced in 4 articles
[sw10110]
 generic libraries of infrastructure for firstorder 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...

GaussJordan
 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 lowlevel 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 boundaryelement software library of...

ACRITHXSC
 Referenced in 49 articles
[sw00015]
 ACRITHXSC is a Fortranlike programming language...

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