
ETPS
 Referenced in 127 articles
[sw06302]
 prover for firstorder logic and type theory. The latter is a cutdown version ... various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic...

Agda
 Referenced in 92 articles
[sw09689]
 proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed ... with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This...

LEGO
 Referenced in 53 articles
[sw09685]
 Jersey ML. It implements various related type systems  the Edinburgh Logical Framework (LF), the Calculus ... Constructions (GCC) and the Unified Theory of Dependent Types (UTT). LEGO is a powerful tool ... higherorder power of its underlying type theories, and the support of specifying new inductive...

ALF
 Referenced in 45 articles
[sw08603]
 based on MartinLöf’s Monomorphic Type Theory with Explicit Substitution. This thesis describes ... editor based on MartinLöf’s type theory with explicit substitutions. ALF is a general ... sound and complete assuming some basic meta theory properties of the substitution calculus. The algorithm ... objects in such a way that the type checking problem is reduced to a unication...

TPS
 Referenced in 63 articles
[sw00973]
 prover for firstorder logic and type theory. The latter is a cutdown version...

Plastic
 Referenced in 18 articles
[sw07403]
 assistant. Typed LF is a framework type theory, in which other type theories...

IMPS
 Referenced in 26 articles
[sw09143]
 based on a version of simple type theory with partial functions and subtypes. Mathematical specification...

Ynot
 Referenced in 23 articles
[sw12334]
 previous work on Hoare Type Theory (HTT). We show how these axioms can be combined...

Satallax
 Referenced in 16 articles
[sw06849]
 Satallax is Church’s simple type theory with extensionality and choice operators. The SAT solver...

Polyp
 Referenced in 24 articles
[sw09131]
 using an extension of Jones’ theories of qualified types and higherorder polymorphism. The semantics...

LYAPACK
 Referenced in 37 articles
[sw12624]
 Control Problems Users ’ Guide (Version 1.0). Control theory is one of the most rapidly developing ... robust algorithms for many types of dense problems in control theory have become available ... quite a number of approaches for several types of large control problems have been proposed ... class of large problems in control theory. An efficient ADIbased solver for large Lyapunov...

Ivor
 Referenced in 3 articles
[sw06343]
 Ivor, a proof engine. Dependent type theory has several practical applications in the fields ... easy extending and embedding of a type theory based theorem prover in a Haskell application ... simple functional programming language; by using type theory as a core representation, we can construct...

XDuce
 Referenced in 49 articles
[sw12436]
 types (socalled regular expression types) directly correspond to document schemas. XDuce also provides ... features, describe its foundations in the theory of regular tree automata, and present a complete ... core, along with a proof of type safety...

AoPA
 Referenced in 4 articles
[sw09832]
 correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties...

Lean
 Referenced in 2 articles
[sw15148]
 small trusted kernel based on dependent type theory. It aims to bridge the gap between ... used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project...

Mincer
 Referenced in 48 articles
[sw09009]
 Program for multiloop calculations in quantum field theory for the Schoonschip system. We present ... threeloop Feynman diagrams of the propagator type within dimensional regularization. The program calculates Laurent...

HOLBoogie
 Referenced in 9 articles
[sw00409]
 verify “background theories”, i.e. theories for datatypes used in annotations as well as memory...

ITIP
 Referenced in 23 articles
[sw17966]
 running on MATLAB for verifying all Shannontype information inequalities, namely those implied ... nonnegativity of Shannon’s information measures. The theory is described in [2]. We also refer ... ITIP. These are called nonShannontype inequalities. Examples are the ones reported...

HR
 Referenced in 23 articles
[sw10392]
 proofs of the conjectures. In group theory, for example, the objects of interest ... groups themselves, the concepts include element types, subgroup types, etc., the conjectures include implication ... named after mathematicians Hardy and Ramanujan  performs theory formation in mathematical domains. It works...

UniMath
 Referenced in 1 article
[sw15140]
 formalization of mathematics in the type theories such as the ones used in Coq, Agda ... class of models of such type theories. These “univalent models” led to the new intuition ... resulted in the introduction into the type theory of the concept of hlevel. This ... intuitive behavior one should define propositions as types of hlevel 1 and sets...