• Agda

  • Referenced in 207 articles [sw09689]
  • Agda is a dependently typed functional programming language: It has inductive families, which are similar ... indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode ... characters, and an interactive Emacs interface (the type checker can assist in the development ... with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This...
  • 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 higher-order, dependently-typed programs with side-effects. Coq already includes...
  • Idris

  • Referenced in 37 articles [sw20011]
  • programming language with dependent types. Dependent types allow types to be predicated on values, meaning ... program’s behaviour can be specified precisely in the type. It is compiled, with eager ... Haskell and ML, and include: Full dependent types with dependent pattern matching; Simple foreign function...
  • Irdis

  • Referenced in 22 articles [sw09690]
  • programming language with dependent types. Dependent types allow types to be predicated on values, meaning ... program’s behaviour can be specified precisely in the type. It is compiled, with eager ... Haskell and ML, and include: Full dependent types with dependent pattern matching; where clauses, with...
  • Epigram

  • Referenced in 22 articles [sw09687]
  • Epigram: Practical programming with dependent types. Find the type error in the following Haskell expression ... course: this program is obviously nonsense unless you’re a typechecker. The trouble is that...
  • ALDOR

  • Referenced in 27 articles [sw01220]
  • constructed and manipulated within programs. Pervasive support for dependent types allows static checking of dynamic ... difficulties encountered in widely-used object-oriented programming languages. It allows programs...
  • NewtonLib

  • Referenced in 298 articles [sw04796]
  • presents a scheme to construct adaptive Newton-type algorithms in close connection with an associated ... these algorithms are presented as informal programs in the text. Some ... book. All of the available programs (not only by the author and his group ... license-charge that depends on the referenced software package and the intended usage. Please read...
  • AoPA

  • Referenced in 8 articles [sw09832]
  • Algebra of programming in Agda: dependent types for relational program derivation. Relational program derivation ... rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich ... type checker. We have developed a library, AoPA (Algebra of Programming in Agda ... encode relational derivations in the dependently typed programming language Agda. A program is coupled with...
  • F*

  • Referenced in 20 articles [sw27563]
  • functional programming language with effects aimed at program verification. It puts together the automation ... proof assistant based on dependent types. After verification, F* programs can be extracted to efficient ... type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together ... allow expressing precise and compact specifications for programs, including functional correctness and security properties...
  • Mtac

  • Referenced in 14 articles [sw13075]
  • Mtac: a monad for typed tactic programming in Coq. Effective support for custom proof automation ... theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated ... extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access...
  • Aglet

  • Referenced in 4 articles [sw13305]
  • Security-typed programming within dependently typed programming. Several recent security-typed programming languages, such ... library within a general-purpose dependently typed programming language, Agda. Our library, Aglet, accounts ... existing security-typed programming languages, such as decentralized access control, typed proof-carrying authorization, ephemeral ... Garg and Pfenning’s BL$_{0}$, using dependent types. Second, we implement a proof search...
  • Delphin

  • Referenced in 18 articles [sw21365]
  • type theory designed to support programming using pattern matching and recursion. The main contribution ... which one can program with higher-order, dependently-typed data structures such as proofs...
  • MiniAgda

  • Referenced in 9 articles [sw21183]
  • MiniAgda: integrating sized and dependent types. Sized types are a modular and theoretically well-understood ... track structural descent and guardedness in the type system to make termination checking robust ... proof assistants and programming languages based on dependent type theory, we have implemented a core...
  • AgsyHOL

  • Referenced in 4 articles [sw13302]
  • been established in Agda, a dependently typed programming language. The theorem prover can output solutions...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • Unified Theory of Dependent Types (UTT). LEGO is a powerful tool for interactive proof development ... underlying type theories, and the support of specifying new inductive types, provide an expressive language ... formalization of mathematical problems and program specification and development...
  • Mella

  • Referenced in 1 article [sw09688]
  • Dependently typed programming based on automated theorem proving. Mella is a minimalistic dependently typed programming ... integrations are essential for supporting program development in dependently typed languages. We integrate the equational...
  • BNDSCO

  • Referenced in 50 articles [sw07779]
  • BNDSCO–A program for the numerical solution of optimal control problems. BNDSCO is used ... most important necessary conditions for different types of unconstrained and constrained optimal control problems ... output and for the construction of problem-dependent subroutines. Finally, the performance of BNDSCO...
  • SPICE

  • Referenced in 22 articles [sw01107]
  • SPICE is a general-purpose circuit simulation program for nonlinear dc, nonlinear transient, and linear ... independent voltage and current sources, four types of dependent sources, lossless and lossy transmission lines...
  • Cayenne

  • Referenced in 29 articles [sw09686]
  • number of language concepts. Having dependent types and combined type and value expressions makes ... type level, allowing types to be used as specifications of programs. However, this power comes...
  • SIGNAL

  • Referenced in 52 articles [sw02915]
  • best suited for the design of dependable real-time systems. Synchronous languages enable a very ... SIGNAL. Just as data-types describe the invariants of program modules in functional languages, temporal...