• Agda

  • Referenced in 207 articles [sw09689]
  • based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish ... with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions ... Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT). LEGO...
  • Oyster

  • Referenced in 34 articles [sw19629]
  • Oyster. Martin-Löf type theory provides a formal framework for the construction of verified programs ... both specified and written in the type theory. We describe an implementation of the type...
  • Lean

  • Referenced in 45 articles [sw15148]
  • small trusted kernel based on dependent type theory. It aims to bridge the gap between ... framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean ... currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe...
  • AoPA

  • Referenced in 8 articles [sw09832]
  • thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express...
  • ETPS

  • Referenced in 160 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 ... proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs ... Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic...
  • LLFp

  • Referenced in 4 articles [sw20866]
  • using monads. We extend the constructive dependent type theory of the Logical Framework 𝖫𝖥 with...
  • GQRAT

  • Referenced in 35 articles [sw00373]
  • concern here is with Gauss-type quadrature rules that are exact for a mixture ... integrand. The underlying theory is presented as well as methods for constructing such rational Gauss...
  • TPS

  • Referenced in 73 articles [sw00973]
  • 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 ... proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs...
  • Polyp

  • Referenced in 33 articles [sw09131]
  • Haskell) with a construct for writing polytypic functions. The extended language type checks definitions ... infers the types of all other expressions using an extension of Jones’ theories of qualified...
  • HoTT

  • Referenced in 16 articles [sw15147]
  • basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions ... category theory centered around comma categories and functoriality of various constructions involving comma categories ... quickly. This talk will discuss the various constructions in the HoTT library, as well ... both of Coq and of univalent type theory, which allow our library to compile...
  • CoCasl

  • Referenced in 26 articles [sw13076]
  • process algebra in a natural way: The type system of communications, the syntax of processes ... world of Casl, while the additional coalgebraic constructs of CoCasl cover the various process equivalences ... framework for studying the semantics and proof theory of reactive systems...
  • PiDuce

  • Referenced in 21 articles [sw01418]
  • services technologies by relying on solid theories about process calculi and formal languages ... type system with subtyping, a pattern matching mechanism for deconstructing XML values, and control constructs...
  • CoqMTU

  • Referenced in 3 articles [sw19138]
  • study a complex type theory, a Calculus of Inductive Constructions with a predicative hierarchy ... built in its conversion relation. The theory T is specified abstractly ... weak-elimination, implying the decidability of type-checking in this case as well as consistency...
  • Ivor

  • Referenced in 3 articles [sw06343]
  • language; by using type theory as a core representation, we can construct and evaluate terms...
  • UniMath

  • Referenced in 23 articles [sw15140]
  • resulted in the introduction into the type theory of the concept of h-level. This ... define propositions as types of h-level 1 and sets as types of h-level ... then *defines* a type hProp(U) - the type of types of h-level ... type hSet(U) - the type of types of h-level 2 in U. With types...
  • TituRel

  • Referenced in 8 articles [sw08501]
  • games, (bi-)simulations, topology, qualitative fuzzy considerations, theory extraction, social choice, decision support via interval ... proofs and transformations. Its generic construction of dependent types make it also a field...
  • Kleene Algebra

  • Referenced in 8 articles [sw32203]
  • their most important models as axiomatic type classes in Isabelle/HOL. Kleene algebras are foundational structures ... from automata and language theory to computational modeling, program construction and verification. We start with...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • first-order logic.\parIts verification conditions -- constructed via a wp calculus from these annotations ... also to verify “background theories”, i.e. theories for data-types used in annotations as well...
  • Globular

  • Referenced in 6 articles [sw18031]
  • theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with ... point-and-click interface, and performs type checking to prevent incorrect rewrites. Hosted...