- Referenced in 205 articles
- 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...
- Referenced in 107 articles
- 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...
- Referenced in 866 articles
- 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...
- Referenced in 450 articles
- dependent variables.Predefined multiphysics-application templates solve many common problem types. You also have the option...
- Referenced in 36 articles
- 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...
- Referenced in 35 articles
- 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...
- Referenced in 29 articles
- 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...
- Referenced in 45 articles
- small trusted kernel based on dependent type theory. It aims to bridge the gap between...
- Referenced in 21 articles
- 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...
- Referenced in 34 articles
- 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...
- Referenced in 20 articles
- 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...
- Referenced in 27 articles
- 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...
- Referenced in 22 articles
- Epigram: Practical programming with dependent types. Find the type error in the following Haskell expression...
- Referenced in 19 articles
- λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules...
- Referenced in 18 articles
- other level is T+! , a type theory designed to support programming using pattern matching ... program with higher-order, dependently-typed data structures such as proofs and typing derivations...
- Referenced in 12 articles
- 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...
- Referenced in 11 articles
- build a proven-correct compiler for dependently-typed, functional languages, such as Gallina—the core ... foundational questions about compilers for dependently-typed languages...
- Referenced in 14 articles
- 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...
- Referenced in 9 articles
- MiniAgda: integrating sized and dependent types. Sized types are a modular and theoretically well-understood ... 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...
- Referenced in 269 articles
- Additionally, they can make available new results. Depending on the progress made in the field ... further improvements in the area of project type scheduling...