Packages tagged dependent-types

30 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (21), bsd3 (18), program (14), data (7), deprecated (2), public-domain (2), benchmark (1), compilers-interpreters (1), configuration (1), data-structures (1), development (1), gpl (1), ...

Agda2512.5A dependently typed functional programming language and proof assistant (dependent-types, library, program)AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell
Agda-executable (deprecated in favor of Agda)660.0Command-line program for type-checking and compiling Agda programs (dependent-types, deprecated, program)NilsAndersDanielsson, UlfNorell
MiniAgda310.0A toy dependently typed programming language with type-based termination. (dependent-types, program)AndreasAbel
PandocAgda130.0Pandoc support for literate Agda (bsd3, dependent-types, library, program)PeterDivianszky
Sit170.0Prototypical type checker for Type Theory with Sized Natural Numbers (dependent-types, program)AndreasAbel
agda-server110.0Http server for Agda (prototype) (bsd3, dependent-types, program)PeterDivianszky
agda-snippets160.0Render just the Agda snippets of a literate Agda file to HTML (bsd3, dependent-types, library, program)LiamOConnorDavis
agda-snippets-hakyll210.0Literate Agda support using agda-snippets, for Hakyll pages. (bsd3, dependent-types, library)LiamOConnorDavis
compare-type80.0compare types of any kinds in haskell (bsd3, dependent-types, library)Kinokkory
cubical150.0Implementation of Univalence in Cubical Sets (dependent-types, mit, program)AndersMortberg
dependent-map482.0Dependent finite maps (partial dependent products) (data, dependent-types, library)JamesCook, RyanTrinkle
dependent-sum482.0Dependent sum type (data, dependent-types, library, public-domain)JamesCook, RyanTrinkle
eliminators120.0Dependently typed elimination functions using singletons (bsd3, dependent-types, library)ryanglscott
helf70.0Typechecking terms of the Edinburgh Logical Framework (LF). (dependent-types, program)AndreasAbel
hoq40.0A language based on homotopy type theory with an interval type (dependent-types, gpl, program)valis
idris2000.0Functional Programming Language with Dependent Types (bsd3, compilers-interpreters, dependent-types, library, program)EdwinBrady
ivor (deprecated in favor of idris)200.0Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)EdwinBrady, GwernBranwen
nanoAgda50.0A toy dependently-typed language (dependent-types, program)JeanPhilippeBernardy
open-typerep140.0Open type representations and dynamic types (benchmark, bsd3, dependent-types, library)EmilAxelsson
pisigma130.0A dependently typed core language (bsd3, dependent-types, development, language, library, program)AndresLoeh, DarinMorrison
prim-uniq110.0Opaque unique identifiers in primitive state monads (data, dependent-types, library, public-domain)JamesCook, RyanTrinkle
reflection15782.25Reifies arbitrary terms into types that can be reflected back into terms (bsd3, data, dependent-types, library, reflection)EdwardKmett
show-type40.0convert types into string values in haskell (bsd3, dependent-types, library)Kinokkory
singleton-dict30.0Typelevel balanced search trees via a singletonized Data.Map (bsd3, data, dependent-types, library)ArieMiddelkoop
singleton-nats120.0Unary natural numbers relying on the singletons infrastructure. (bsd3, data, dependent-types, library)AndrasKovacs
singletons902.5A framework for generating singleton types (bsd3, dependent-types, library)RichardEisenberg, ryanglscott
type-fun480.0Collection of widely reimplemented type families (bsd3, dependent-types, library)AlekseyUymanov
type-level-bst10.0type-level binary search trees in haskell (bsd3, data-structures, dependent-types, library)Kinokkory
typeparams80.0Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation (bsd3, configuration, data, dependent-types, library, optimization)MikeIzbicki
uAgda130.0A simplistic dependently-typed language with parametricity. (dependent-types, program)JeanPhilippeBernardy