
Agda
 Referenced in 171 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 106 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 686 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 337 articles
[sw04091]
 dependent variables.Predefined multiphysicsapplication templates solve many common problem types. You also have the option...

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...

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

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...

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

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

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

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 11 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...

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

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 typetheoretic machinery that is not easily integrated ... powerful extension to Coq that supports dependentlytyped tactic programming. Mtac tactics have access...

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

MiniAgda
 Referenced in 8 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...

SPICE
 Referenced in 20 articles
[sw01107]
 independent voltage and current sources, four types of dependent sources, lossless and lossy transmission lines...