• ETPS

  • Referenced in 128 articles [sw06302]
  • prover for first-order logic and type theory. The latter is a cut-down 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 104 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 58 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 ... higher-order power of its underlying type theories, and the support of specifying new inductive...
  • ALF

  • Referenced in 50 articles [sw08603]
  • based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. This thesis describes ... editor based on Martin-Lö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 65 articles [sw00973]
  • prover for first-order logic and type theory. The latter is a cut-down version...
  • Oyster

  • Referenced in 23 articles [sw19629]
  • program synthesis with Oyster. Martin-Lö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 30 articles [sw09143]
  • based on a version of simple type theory with partial functions and subtypes. Mathematical specification...
  • Plastic

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

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

  • Referenced in 22 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 higher-order polymorphism. The semantics...
  • LYAPACK

  • Referenced in 39 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 ADI-based solver for large Lyapunov...
  • Lean

  • Referenced in 4 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...
  • 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...
  • AoPA

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

  • Referenced in 49 articles [sw12436]
  • types (so-called 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...
  • PAL+

  • Referenced in 2 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 Martin-Löf’s type theory ... that are intuitively in the object type theories: types and their objects, and families ... correct meta-language for specifying type theories (e.g., dependent type theories...
  • scunac

  • Referenced in 3 articles [sw21328]
  • untyped set theory. Using the dependent type theory of Scunak, we can define object level ... between functions in the (meta-level) type theory and (object-level) functional relations. The encoding...
  • MiniAgda

  • Referenced in 4 articles [sw21183]
  • programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with ... considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which...
  • UniMath

  • Referenced in 2 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 h-level. This ... intuitive behavior one should define propositions as types of h-level 1 and sets...