Packages tagged dependent-types
52 packages have this tag.
[Merge tag] (trustees only)Related tags: library (42), bsd3 (34), data (18), program (17), gpl (5), singletons (5), deprecated (4), mit (4), data-structures (2), development (2), language (2), lens (2), math (2), optics (2), ...
Name |
DLs |
Rating |
Description |
Tags |
Last U/L |
Maintainer |
|---|---|---|---|---|---|---|
| Agda | 376 | 2.75 | A dependently typed functional programming language and proof assistant | (dependent-types, program) | 2022-04-02 | AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell |
| Agda-executable (deprecated in favor of Agda) | 34 | 0.0 | Command-line program for type-checking and compiling Agda programs | (dependent-types, deprecated, program) | 2012-03-12 | NilsAndersDanielsson, UlfNorell |
| MiniAgda | 44 | 2.0 | A toy dependently typed programming language with type-based termination. | (dependent-types, mit, program) | 2022-03-11 | AndreasAbel |
| PandocAgda | 9 | 0.0 | Pandoc support for literate Agda | (bsd3, dependent-types, library, program) | 2013-03-11 | PeterDivianszky |
| Sit | 14 | 0.0 | Prototypical type checker for Type Theory with Sized Natural Numbers | (dependent-types, library, program) | 2022-03-18 | AndreasAbel |
| agda-server | 15 | 0.0 | Http server for Agda (prototype) | (bsd3, dependent-types, program) | 2013-10-03 | PeterDivianszky |
| agda-snippets (deprecated in favor of Agda) | 13 | 0.0 | Render just the Agda snippets of a literate Agda file to HTML | (bsd3, dependent-types, deprecated, library, program) | 2017-06-04 | LiamOConnorDavis |
| agda-snippets-hakyll (deprecated in favor of Agda) | 11 | 0.0 | Literate Agda support using agda-snippets, for Hakyll pages. | (bsd3, dependent-types, deprecated, library) | 2017-06-04 | LiamOConnorDavis |
| agda-unused | 7 | 0.0 | Check for unused code in an Agda project. | (dependent-types, library, mit, program) | 2021-05-05 | msuperdock |
| agda2lagda | 12 | 0.0 | Translate .agda files into .lagda.tex files. | (dependent-types, development, program) | 2021-06-01 | AndreasAbel |
| bin | 407 | 0.0 | Bin: binary natural numbers. | (data, dependent-types, gpl, library, math, singletons) | 2022-01-03 | phadej |
| compare-type | 7 | 0.0 | compare types of any kinds in haskell | (bsd3, dependent-types, library) | 2015-01-10 | Kinokkory |
| cubical | 20 | 0.0 | Implementation of Univalence in Cubical Sets | (dependent-types, mit, program) | 2014-04-27 | AndersMortberg |
| dec | 448 | 0.0 | Decidable propositions. | (bsd3, data, dependent-types, library) | 2021-02-20 | phadej |
| decidable | 19 | 0.0 | Combinators for manipulating dependently-typed predicates. | (bsd3, dependent-types, library) | 2020-02-03 | jle |
| dependent-map | 407 | 2.5 | Dependent finite maps (partial dependent products) | (data, dependent-types, library) | 2020-03-27 | BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch |
| dependent-sum | 551 | 2.25 | Dependent sum type | (data, dependent-types, library, public-domain) | 2020-03-25 | BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch, DanBornside |
| eliminators | 25 | 0.0 | Dependently typed elimination functions using singletons | (bsd3, dependent-types, library) | 2021-10-31 | ryanglscott |
| fin | 454 | 2.0 | Nat and Fin: peano naturals and finite numbers | (bsd3, data, dependent-types, library, math, singletons) | 2022-01-03 | phadej |
| helf | 8 | 0.0 | Typechecking terms of the Edinburgh Logical Framework (LF). | (dependent-types, mit, program) | 2021-08-12 | AndreasAbel |
| hoq | 2 | 0.0 | A language based on homotopy type theory with an interval type | (dependent-types, gpl, program) | 2014-09-27 | valis |
| idris | 215 | 2.25 | Functional Programming Language with Dependent Types | (bsd3, compilers-interpreters, dependent-types, library, program) | 2021-10-22 | EdwinBrady, niklasl |
| instance-map | 6 | 0.0 | Template haskell utilities for helping with deserialization etc. of existential types | (bsd3, dependent-types, library) | 2018-07-23 | rwarfield |
| ivor (deprecated in favor of idris) | 21 | 0.0 | Theorem proving library based on dependent type theory | (bsd3, dependent-types, deprecated, library, theorem-provers) | 2011-06-16 | EdwinBrady, GwernBranwen |
| lens-typelevel | 5 | 0.0 | Type-level lenses using singletons | (bsd3, dependent-types, lenses, library) | 2018-10-29 | jle |
| list-witnesses | 12 | 0.0 | Witnesses for working with type-level lists | (bsd3, dependent-types, library) | 2019-08-26 | jle |
| nanoAgda | 6 | 0.0 | A toy dependently-typed language | (dependent-types, program) | 2012-03-20 | JeanPhilippeBernardy |
| open-typerep | 22 | 0.0 | Open type representations and dynamic types | (bsd3, dependent-types, library) | 2016-05-27 | EmilAxelsson |
| parameterized-utils | 194 | 2.0 | Classes and data structures for working with data-kind indexed types | (bsd3, data-structures, dependent-types, library) | 2022-03-08 | KevinQuick, RobertDockins, galoisinc |
| pisigma | 16 | 0.0 | A dependently typed core language | (bsd3, dependent-types, development, language, library, program) | 2011-05-18 | AndresLoeh, DarinMorrison |
| prim-uniq | 95 | 0.0 | Opaque unique identifiers in primitive state monads | (data, dependent-types, library, public-domain) | 2020-04-15 | BertramFelgenhauer, JamesCook, RyanTrinkle |
| ral | 395 | 0.0 | Random access lists | (data, dependent-types, gpl, library, singletons) | 2022-01-03 | phadej |
| ral-lens | 8 | 0.0 | Length-indexed random access lists: lens utilities. | (data, dependent-types, gpl, lens, library, singletons) | 2021-02-28 | phadej |
| ral-optics | 3 | 0.0 | Length-indexed random access lists: optics utilities. | (data, dependent-types, gpl, library, optics, singletons) | 2021-02-28 | phadej |
| reflection | 580 | 2.25 | Reifies arbitrary terms into types that can be reflected back into terms | (bsd3, data, dependent-types, library, reflection) | 2020-05-16 | EdwardKmett, ryanglscott |
| show-type | 14 | 0.0 | convert types into string values in haskell | (bsd3, dependent-types, library) | 2015-01-08 | Kinokkory |
| singleton-dict | 7 | 0.0 | Typelevel balanced search trees via a singletonized Data.Map | (bsd3, data, dependent-types, library) | 2017-06-09 | ArieMiddelkoop |
| singleton-nats | 40 | 0.0 | Unary natural numbers relying on the singletons infrastructure. | (bsd3, data, dependent-types, library) | 2021-03-12 | AndrasKovacs, ryanglscott |
| singletons | 337 | 2.75 | Basic singleton types and definitions | (bsd3, dependent-types, library) | 2021-10-31 | RichardEisenberg, ryanglscott |
| singletons-base | 59 | 0.0 | A promoted and singled version of the base library | (bsd3, dependent-types, library) | 2021-10-31 | ryanglscott |
| singletons-th | 74 | 0.0 | A framework for generating singleton types | (bsd3, dependent-types, library) | 2021-10-31 | ryanglscott |
| some | 682 | 0.0 | Existential type: Some | (bsd3, data, dependent-types, library) | 2021-04-05 | RyanTrinkle, phadej |
| symbols | 30 | 0.0 | Symbol manipulation | (bsd3, dependent-types, library) | 2019-09-10 | kcsongor |
| tensor-safe | 6 | 2.0 | Create valid deep neural network architectures | (ai, bsd3, dependent-types, language, library, program) | 2019-05-03 | leopiney |
| type-equality | 430 | 0.0 | Data.Type.Equality compat package | (bsd3, data, dependent-types, library) | 2019-09-06 | ErikHesselink, phadej, ryanglscott |
| type-fun | 33 | 0.0 | Collection of widely reimplemented type families | (bsd3, dependent-types, library) | 2021-06-04 | AlekseyUymanov |
| type-level-bst | 9 | 0.0 | type-level binary search trees in haskell | (bsd3, data-structures, dependent-types, library) | 2014-10-28 | Kinokkory |
| typeparams | 13 | 0.0 | Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation | (bsd3, configuration, data, dependent-types, library, optimization) | 2015-01-26 | MikeIzbicki |
| uAgda | 25 | 0.0 | A simplistic dependently-typed language with parametricity. | (dependent-types, program) | 2012-03-10 | JeanPhilippeBernardy |
| vec | 73 | 0.0 | Vec: length-indexed (sized) list | (bsd3, data, dependent-types, library) | 2022-01-03 | phadej |
| vec-lens | 11 | 0.0 | Vec: length-indexed (sized) list: lens support | (bsd3, data, dependent-types, lens, library) | 2021-02-28 | phadej |
| vec-optics | 9 | 0.0 | Vec: length-indexed (sized) list: optics support | (bsd3, data, dependent-types, library, optics) | 2021-02-28 | phadej |