• Agda

  • Referenced in 158 articles [sw09689]
  • Agda is a dependently typed functional programming language: It has inductive families, which are similar ... checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics ... with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This...
  • LEGO

  • Referenced in 105 articles [sw09685]
  • Jersey ML. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus ... Unified Theory of Dependent Types (UTT). LEGO is a powerful tool for interactive proof development...
  • HE-E1GODF

  • Referenced in 618 articles [sw06606]
  • Riemann solver to solve the time-dependent one dimensional Euler equations for an ideal ... approximate Rieman solvers of the approximate flux type: Roe Riemann solver, HLLC Riemann solver...
  • Ynot

  • Referenced in 32 articles [sw12334]
  • Ynot, dependent types for imperative programs. We describe an axiomatic extension to the Coq proof ... reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes ... powerful functional language that supports dependent types, but that language is limited to pure, total...
  • Idris

  • Referenced in 28 articles [sw20011]
  • purpose pure functional programming language with dependent types. Dependent types allow types to be predicated ... behaviour can be specified precisely in the type. It is compiled, with eager evaluation ... Haskell and ML, and include: Full dependent types with dependent pattern matching; Simple foreign function ... lambda bindings; Dependent records with projection and update; Interfaces (similar to type classes in Haskell...
  • COMSOL

  • Referenced in 294 articles [sw04091]
  • dependent variables.Predefined multiphysics-application templates solve many common problem types. You also have the option...
  • Cayenne

  • Referenced in 29 articles [sw09686]
  • Cayenne — a language with dependent types. Cayenne is a Haskell-like language. The main difference ... Cayenne is that Cayenne has dependent types, i.e., the result type of a function ... record components (which can be types or values) may depend on other components. Cayenne also ... number of language concepts. Having dependent types and combined type and value expressions makes...
  • GF

  • Referenced in 31 articles [sw13667]
  • formal languages. Grammatical objects have a type system, which helps to eliminate run-time errors ... uses dependent types in abstract syntax to express semantic conditions, such as well-typedness...
  • ALDOR

  • Referenced in 24 articles [sw01220]
  • used more in other settings.In Aldor, types and functions are first class values that ... manipulated within programs. Pervasive support for dependent types allows static checking of dynamic objects. What...
  • F*

  • Referenced in 16 articles [sw27563]
  • proof assistant based on dependent types. After verification, F* programs can be extracted to efficient ... primitives. F*’s type system includes dependent types, monadic effects, refinement types, and a weakest...
  • Epigram

  • Referenced in 21 articles [sw09687]
  • Epigram: Practical programming with dependent types. Find the type error in the following Haskell expression...
  • Lean

  • Referenced in 17 articles [sw15148]
  • small trusted kernel based on dependent type theory. It aims to bridge the gap between...
  • Delphin

  • Referenced in 16 articles [sw21365]
  • other level is T+! [15], a type theory designed to support programming using pattern matching ... program with higher-order, dependently-typed data structures such as proofs and typing derivations...
  • Coquelicot

  • Referenced in 10 articles [sw11552]
  • integrals and derivatives are based on dependent types, which make them especially cumbersome ... total functions in place of dependent types for limits, derivatives, integrals, power series...
  • AoPA

  • Referenced in 8 articles [sw09832]
  • Algebra of programming in Agda: dependent types for relational program derivation. Relational program derivation ... obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various ... correctness properties to be verified by the type checker. We have developed a library, AoPA ... encode relational derivations in the dependently typed programming language Agda. A program is coupled with...
  • Mtac

  • Referenced in 13 articles [sw13075]
  • theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated ... powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access...
  • dedukti

  • Referenced in 13 articles [sw13663]
  • λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules...
  • CertiCoq

  • Referenced in 9 articles [sw22728]
  • build a proven-correct compiler for dependently-typed, functional languages, such as Gallina—the core ... foundational questions about compilers for dependently-typed languages...
  • SafeDpi

  • Referenced in 13 articles [sw01989]
  • incoming port. We define a sophisticated static type system for these ports, which restrict ... processes launched by incoming code. Dependent and existential types are used to add flexibility, allowing ... these launched processes, encoded as process types, to depend on the host’s instantiation ... characterised coinductively, using bisimulations based on typed actions. The characterisation is based on the idea...
  • Irdis

  • Referenced in 6 articles [sw09690]
  • Irdis: a language with dependent types. Idris is a general purpose pure functional programming language ... with dependent types. Dependent types allow types to be predicated on values, meaning that some ... Haskell and ML, and include: Full dependent types with dependent pattern matching; where clauses, with ... lambda bindings; Dependent records with projection and update; Type classes; Monad comprehensions; Syntactic conveniences...