
Agda
 Referenced in 205 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 107 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...

HEE1GODF
 Referenced in 866 articles
[sw06606]
 Riemann solver to solve the timedependent one dimensional Euler equations for an ideal ... approximate Rieman solvers of the approximate flux type: Roe Riemann solver, HLLC Riemann solver...

COMSOL
 Referenced in 450 articles
[sw04091]
 dependent variables.Predefined multiphysicsapplication templates solve many common problem types. You also have the option...

Idris
 Referenced in 36 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...

Ynot
 Referenced in 35 articles
[sw12334]
 Ynot, dependent types for imperative programs. We describe an axiomatic extension to the Coq proof ... reasoning about, and extracting higherorder, dependentlytyped programs with sideeffects. Coq already includes ... powerful functional language that supports dependent types, but that language is limited to pure, total...

Cayenne
 Referenced in 29 articles
[sw09686]
 Cayenne — a language with dependent types. Cayenne is a Haskelllike 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...

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

Irdis
 Referenced in 21 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...

GF
 Referenced in 34 articles
[sw13667]
 formal languages. Grammatical objects have a type system, which helps to eliminate runtime errors ... uses dependent types in abstract syntax to express semantic conditions, such as welltypedness...

F*
 Referenced in 20 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...

ALDOR
 Referenced in 27 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...

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

dedukti
 Referenced in 19 articles
[sw13663]
 λΠmodulo calculus, a dependently typed λcalculus with the addition of typed rewrite rules...

Delphin
 Referenced in 18 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...

Coquelicot
 Referenced in 12 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...

CertiCoq
 Referenced in 11 articles
[sw22728]
 build a provencorrect compiler for dependentlytyped, functional languages, such as Gallina—the core ... foundational questions about compilers for dependentlytyped languages...

Mtac
 Referenced in 14 articles
[sw13075]
 theorem prover, or (b) rely on advanced typetheoretic machinery that is not easily integrated ... powerful extension to Coq that supports dependentlytyped tactic programming. Mtac tactics have access...

MiniAgda
 Referenced in 9 articles
[sw21183]
 MiniAgda: integrating sized and dependent types. Sized types are a modular and theoretically wellunderstood ... assistants and programming languages based on dependent type theory, we have implemented a core language ... were necessary to soundly integrate sized types with dependencies and pattern matching, which was made...

PSPLIB
 Referenced in 269 articles
[sw00740]
 Additionally, they can make available new results. Depending on the progress made in the field ... further improvements in the area of project type scheduling...