Packages tagged dependent-types
57 packages have this tag.
[Merge tag] (trustees only)Related tags: library (47), bsd3 (36), data (19), program (19), deprecated (6), gpl (6), mit (6), singletons (5), data-structures (2), development (2), language (2), lens (2), math (2), optics (2), public-domain (2), ai (1), compilers-interpreters (1), ...
Name |
DLs |
Rating |
Rev Deps |
Description |
Tags |
Last U/L |
Last Version |
Maintainers |
|---|---|---|---|---|---|---|---|---|
| Agda | 414 | 2.75 | 8 | A dependently typed functional programming language and proof assistant | (dependent-types, mit, program) | 2024-09-12 | 2.7.0.1 | AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell |
| Agda-executable (deprecated in favor of Agda) | 13 | 0.0 | 1 | Command-line program for type-checking and compiling Agda programs | (dependent-types, deprecated, program) | 2012-03-12 | 2.3.0.1 | NilsAndersDanielsson, UlfNorell |
| MiniAgda | 14 | 2.0 | 1 | A toy dependently typed programming language with type-based termination. | (dependent-types, mit, program) | 2022-03-11 | 0.2022.3.11 | AndreasAbel |
| PandocAgda (deprecated) | 5 | 0.0 | 1 | Pandoc support for literate Agda | (bsd3, dependent-types, deprecated, library, program) | 2013-03-11 | 2.3.3.0.2 | PeterDivianszky |
| Sit | 12 | 0.0 | 1 | Prototypical type checker for Type Theory with Sized Natural Numbers | (dependent-types, library, program) | 2023-08-03 | 0.2023.8.3 | AndreasAbel |
| aeson-dependent-sum | 2 | 0.0 | 0 | JSON encoding/decoding for dependent-sum | (data, dependent-types, gpl, json, library) | 2022-08-27 | 0.1.0.1 | jack |
| agda-server (deprecated) | 5 | 0.0 | 1 | Http server for Agda (prototype) | (bsd3, dependent-types, deprecated, program) | 2013-10-03 | 0.1.1 | PeterDivianszky |
| agda-snippets (deprecated in favor of Agda) | 7 | 0.0 | 1 | Render just the Agda snippets of a literate Agda file to HTML | (bsd3, dependent-types, deprecated, library, program) | 2017-06-04 | 2.5.2 | LiamOConnorDavis |
| agda-snippets-hakyll (deprecated in favor of Agda) | 14 | 0.0 | 1 | Literate Agda support using agda-snippets, for Hakyll pages. | (bsd3, dependent-types, deprecated, library) | 2017-06-04 | 0.1.2.2 | LiamOConnorDavis |
| agda-unused | 3 | 0.0 | 0 | Check for unused code in an Agda project. | (dependent-types, library, mit, program) | 2022-11-26 | 0.3.0 | msuperdock |
| agda2lagda | 12 | 0.0 | 0 | Translate .agda files into .lagda.tex files. | (dependent-types, development, program) | 2023-06-09 | 0.2023.6.9 | AndreasAbel |
| bin | 206 | 0.0 | 5 | Bin: binary natural numbers. | (data, dependent-types, gpl, library, math, singletons) | 2024-06-08 | 0.1.4 | phadej |
| compare-type | 9 | 0.0 | 1 | compare types of any kinds in haskell | (bsd3, dependent-types, library) | 2015-01-10 | 0.1.1 | Kinokkory |
| cubical | 7 | 0.0 | 1 | Implementation of Univalence in Cubical Sets | (dependent-types, mit, program) | 2014-04-27 | 0.2.0 | AndersMortberg |
| dec | 294 | 0.0 | 4 | Decidable propositions. | (bsd3, data, dependent-types, library) | 2024-05-17 | 0.0.6 | phadej |
| decidable | 29 | 0.0 | 2 | Combinators for manipulating dependently-typed predicates. | (bsd3, dependent-types, library) | 2024-02-28 | 0.3.1.1 | jle |
| dependent-map | 194 | 2.5 | 39 | Dependent finite maps (partial dependent products) | (data, dependent-types, library) | 2020-03-27 | 0.4.0.0 | BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch, alexfmpe, maralorn, ymeister |
| dependent-sum | 264 | 2.25 | 63 | Dependent sum type | (data, dependent-types, library, public-domain) | 2022-12-22 | 0.7.2.0 | BertramFelgenhauer, JamesCook, JohnEricson, RyanTrinkle, abrar, 3noch, alexfmpe, maralorn, DanBornside, ymeister |
| eliminators | 28 | 0.0 | 1 | Dependently typed elimination functions using singletons | (bsd3, dependent-types, library) | 2024-05-12 | 0.9.5 | ryanglscott |
| fin | 209 | 2.0 | 14 | Nat and Fin: peano naturals and finite numbers | (bsd3, data, dependent-types, library, math, singletons) | 2024-06-08 | 0.3.1 | phadej |
| helf | 8 | 0.0 | 1 | Typechecking terms of the Edinburgh Logical Framework (LF). | (dependent-types, mit, program) | 2024-03-18 | 1.0.20240318 | AndreasAbel |
| hoq | 4 | 0.0 | 1 | A language based on homotopy type theory with an interval type | (dependent-types, gpl, program) | 2014-09-27 | 0.3 | valis |
| idris | 104 | 2.25 | 1 | Functional Programming Language with Dependent Types | (bsd3, compilers-interpreters, dependent-types, library, program) | 2021-10-22 | 1.3.4 | EdwinBrady, niklasl |
| instance-map | 2 | 0.0 | 1 | Template haskell utilities for helping with deserialization etc. of existential types | (bsd3, dependent-types, library) | 2018-07-23 | 0.1.0.0 | rwarfield |
| ivor (deprecated in favor of idris) | 4 | 0.0 | 2 | Theorem proving library based on dependent type theory | (bsd3, dependent-types, deprecated, library, theorem-provers) | 2011-06-16 | 0.1.14.1 | EdwinBrady, GwernBranwen |
| lens-typelevel | 4 | 0.0 | 1 | Type-level lenses using singletons | (bsd3, dependent-types, lenses, library) | 2018-10-29 | 0.1.1.0 | jle |
| list-witnesses | 15 | 0.0 | 0 | Witnesses for working with type-level lists | (bsd3, dependent-types, library) | 2024-02-28 | 0.1.4.1 | jle |
| nanoAgda | 4 | 0.0 | 1 | A toy dependently-typed language | (dependent-types, program) | 2012-03-20 | 1.0.0 | JeanPhilippeBernardy |
| open-typerep | 25 | 0.0 | 2 | Open type representations and dynamic types | (bsd3, dependent-types, library) | 2016-05-27 | 0.6.1 | EmilAxelsson |
| parameterized-utils | 78 | 2.0 | 13 | Classes and data structures for working with data-kind indexed types | (bsd3, data-structures, dependent-types, library) | 2024-01-15 | 2.1.8.0 | KevinQuick, RobertDockins, ryanglscott, galoisinc, mccleeary |
| path-sing | 2 | 0.0 | 0 | A singleton wrapper for the `path` library. | (dependent-types, filesystem, library, mpl, system) | 2023-09-18 | 0.1.0.0 | YamadaRyo |
| pisigma | 7 | 0.0 | 1 | A dependently typed core language | (bsd3, dependent-types, development, language, library, program) | 2011-05-18 | 0.2.1 | AndresLoeh, DarinMorrison |
| prim-uniq | 45 | 0.0 | 4 | Opaque unique identifiers in primitive state monads | (data, dependent-types, library, public-domain) | 2020-04-15 | 0.2 | BertramFelgenhauer, JamesCook, RyanTrinkle |
| proof-assistant-bot | 3 | 0.0 | 0 | Telegram bot for proof assistants | (dependent-types, library, mit, program) | 2024-02-07 | 0.2.2 | swamp_agr |
| ral | 195 | 0.0 | 4 | Random access lists | (data, dependent-types, gpl, library, singletons) | 2024-06-08 | 0.2.2 | phadej |
| ral-lens | 20 | 0.0 | 0 | Length-indexed random access lists: lens utilities. | (data, dependent-types, gpl, lens, library, singletons) | 2024-06-08 | 0.2.1 | phadej |
| ral-optics | 7 | 0.0 | 0 | Length-indexed random access lists: optics utilities. | (data, dependent-types, gpl, library, optics, singletons) | 2024-06-08 | 0.2.1 | phadej |
| reflection | 418 | 2.25 | 94 | Reifies arbitrary terms into types that can be reflected back into terms | (bsd3, data, dependent-types, library, reflection) | 2024-05-04 | 2.1.8 | EdwardKmett, ryanglscott |
| rzk | 52 | 2.0 | 1 | An experimental proof assistant for synthetic ∞-categories | (bsd3, dependent-types, library, program) | 2024-08-18 | 0.7.5 | NickolayKudasov |
| show-type | 7 | 0.0 | 4 | convert types into string values in haskell | (bsd3, dependent-types, library) | 2015-01-08 | 0.1.1 | Kinokkory |
| singleton-bool | 322 | 0.0 | 6 | Type level booleans | (bsd3, dependent-types, library) | 2024-06-04 | 0.1.8 | phadej |
| singleton-dict | 3 | 0.0 | 1 | Typelevel balanced search trees via a singletonized Data.Map | (bsd3, data, dependent-types, library) | 2017-06-09 | 0.1.0.0 | ArieMiddelkoop |
| singleton-nats | 87 | 0.0 | 2 | Unary natural numbers relying on the singletons infrastructure. | (bsd3, data, dependent-types, library) | 2023-10-13 | 0.4.7 | AndrasKovacs, ryanglscott |
| singletons | 198 | 2.75 | 121 | Basic singleton types and definitions | (bsd3, dependent-types, library) | 2024-05-12 | 3.0.3 | RichardEisenberg, ryanglscott |
| singletons-base | 147 | 0.0 | 26 | A promoted and singled version of the base library | (bsd3, dependent-types, library) | 2024-05-12 | 3.4 | ryanglscott |
| singletons-th | 181 | 0.0 | 9 | A framework for generating singleton types | (bsd3, dependent-types, library) | 2024-05-12 | 3.4 | ryanglscott |
| some | 370 | 0.0 | 30 | Existential type: Some | (bsd3, data, dependent-types, library) | 2023-10-24 | 1.0.6 | phadej |
| symbols | 23 | 0.0 | 3 | Symbol manipulation | (bsd3, dependent-types, library) | 2019-09-10 | 0.3.0.0 | kcsongor |
| tensor-safe | 3 | 2.0 | 0 | Create valid deep neural network architectures | (ai, bsd3, dependent-types, language, library, program) | 2019-05-03 | 0.1.0.1 | leopiney |
| type-equality | 182 | 0.0 | 14 | Data.Type.Equality compat package | (bsd3, data, dependent-types, library) | 2024-05-12 | 1.0.1 | ErikHesselink, phadej, ryanglscott |
| type-fun | 17 | 0.0 | 5 | Collection of widely reimplemented type families | (bsd3, dependent-types, library) | 2021-06-04 | 0.1.3 | AlekseyUymanov |
| type-level-bst | 4 | 0.0 | 1 | type-level binary search trees in haskell | (bsd3, data-structures, dependent-types, library) | 2014-10-28 | 0.1 | Kinokkory |
| typeparams | 18 | 0.0 | 1 | Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation | (bsd3, configuration, data, dependent-types, library, optimization) | 2015-01-26 | 0.0.6 | MikeIzbicki |
| uAgda | 13 | 0.0 | 1 | A simplistic dependently-typed language with parametricity. | (dependent-types, program) | 2012-03-10 | 1.2.0.4 | JeanPhilippeBernardy |
| vec | 59 | 0.0 | 5 | Vec: length-indexed (sized) list | (bsd3, data, dependent-types, library) | 2024-06-08 | 0.5.1 | phadej |
| vec-lens | 12 | 0.0 | 0 | Vec: length-indexed (sized) list: lens support | (bsd3, data, dependent-types, lens, library) | 2024-06-08 | 0.4.1 | phadej |
| vec-optics | 8 | 0.0 | 0 | Vec: length-indexed (sized) list: optics support | (bsd3, data, dependent-types, library, optics) | 2024-06-08 | 0.4.1 | phadej |