
ETPS
 Referenced in 145 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 152 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 103 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 61 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 67 articles
[sw00973]
 prover for firstorder logic and type theory. The latter is a cutdown version...

Oyster
 Referenced in 28 articles
[sw19629]
 program synthesis with Oyster. MartinLöf type theory provides a formal framework for the construction ... both specified and written in the type theory. We describe an implementation of the type...

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

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

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

cubicaltt
 Referenced in 18 articles
[sw22723]
 Cubical type theory. Code library. Experimental implementation of Cubical Type Theory...

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

Lean
 Referenced in 16 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...

LYAPACK
 Referenced in 50 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...

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

Delphin
 Referenced in 16 articles
[sw21365]
 other level is T+! [15], a type theory designed to support programming using pattern matching ... program with higherorder, dependentlytyped data structures such as proofs and typing derivations...

HoTT
 Referenced in 6 articles
[sw15147]
 libraries exploring univalent foundations and homotopy type theory, the other being UniMath. The library includes ... basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions ... Cantor spaces and the surreals, the basic theory of hlevels, and a significant amount ... both of Coq and of univalent type theory, which allow our library to compile...

UniMath
 Referenced in 5 articles
[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...

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

PAL+
 Referenced in 3 articles
[sw21366]
 provide schematic mechanisms for specification of type theories and their use in practice. The framework ... framework for specification and implementation of type theories, such as MartinLöf’s type theory ... that are intuitively in the object type theories: types and their objects, and families ... correct metalanguage for specifying type theories (e.g., dependent type theories...

Nitpick
 Referenced in 46 articles
[sw00622]
 type system and a hotel key card system. Our experimental results on Isabelle theories...