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

HEE1GODF
 Referenced in 618 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...

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

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 higherorder, dependentlytyped 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 typetheoretic machinery that is not easily integrated ... powerful extension to Coq that supports dependentlytyped 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 provencorrect compiler for dependentlytyped, functional languages, such as Gallina—the core ... foundational questions about compilers for dependentlytyped 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...