Packages tagged dependent-types

56 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (46), bsd3 (35), 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
Agda5262.758A dependently typed functional programming language and proof assistant (dependent-types, mit, program)2024-03-062.6.4.3AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell
Agda-executable (deprecated in favor of Agda)200.01Command-line program for type-checking and compiling Agda programs (dependent-types, deprecated, program)2012-03-122.3.0.1NilsAndersDanielsson, UlfNorell
MiniAgda252.01A toy dependently typed programming language with type-based termination. (dependent-types, mit, program)2022-03-110.2022.3.11AndreasAbel
PandocAgda (deprecated)40.01Pandoc support for literate Agda (bsd3, dependent-types, deprecated, library, program)2013-03-112.3.3.0.2PeterDivianszky
Sit190.01Prototypical type checker for Type Theory with Sized Natural Numbers (dependent-types, library, program)2023-08-030.2023.8.3AndreasAbel
aeson-dependent-sum90.00JSON encoding/decoding for dependent-sum (data, dependent-types, gpl, json, library)2022-08-270.1.0.1jack
agda-server (deprecated)80.01Http server for Agda (prototype) (bsd3, dependent-types, deprecated, program)2013-10-030.1.1PeterDivianszky
agda-snippets (deprecated in favor of Agda)130.01Render just the Agda snippets of a literate Agda file to HTML (bsd3, dependent-types, deprecated, library, program)2017-06-042.5.2LiamOConnorDavis
agda-snippets-hakyll (deprecated in favor of Agda)140.01Literate Agda support using agda-snippets, for Hakyll pages. (bsd3, dependent-types, deprecated, library)2017-06-040.1.2.2LiamOConnorDavis
agda-unused80.00Check for unused code in an Agda project. (dependent-types, library, mit, program)2022-11-260.3.0msuperdock
agda2lagda260.00Translate .agda files into .lagda.tex files. (dependent-types, development, program)2023-06-090.2023.6.9AndreasAbel
bin1660.05Bin: binary natural numbers. (data, dependent-types, gpl, library, math, singletons)2023-03-210.1.3phadej
compare-type100.01compare types of any kinds in haskell (bsd3, dependent-types, library)2015-01-100.1.1Kinokkory
cubical120.01Implementation of Univalence in Cubical Sets (dependent-types, mit, program)2014-04-270.2.0AndersMortberg
dec2200.04Decidable propositions. (bsd3, data, dependent-types, library)2022-08-210.0.5phadej
decidable340.02Combinators for manipulating dependently-typed predicates. (bsd3, dependent-types, library)2024-02-280.3.1.1jle
dependent-map2032.536Dependent finite maps (partial dependent products) (data, dependent-types, library)2020-03-270.4.0.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch
dependent-sum3152.2559Dependent sum type (data, dependent-types, library, public-domain)2022-12-220.7.2.0BertramFelgenhauer, JamesCook, JohnEricson, RyanTrinkle, abrar, 3noch, DanBornside
eliminators410.01Dependently typed elimination functions using singletons (bsd3, dependent-types, library)2023-10-130.9.4ryanglscott
fin1682.012Nat and Fin: peano naturals and finite numbers (bsd3, data, dependent-types, library, math, singletons)2023-03-210.3phadej
helf270.01Typechecking terms of the Edinburgh Logical Framework (LF). (dependent-types, mit, program)2024-03-181.0.20240318AndreasAbel
hoq90.01A language based on homotopy type theory with an interval type (dependent-types, gpl, program)2014-09-270.3valis
idris2132.251Functional Programming Language with Dependent Types (bsd3, compilers-interpreters, dependent-types, library, program)2021-10-221.3.4EdwinBrady, niklasl
instance-map40.01Template haskell utilities for helping with deserialization etc. of existential types (bsd3, dependent-types, library)2018-07-230.1.0.0rwarfield
ivor (deprecated in favor of idris)190.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
lens-typelevel80.01Type-level lenses using singletons (bsd3, dependent-types, lenses, library)2018-10-290.1.1.0jle
list-witnesses270.00Witnesses for working with type-level lists (bsd3, dependent-types, library)2024-02-280.1.4.1jle
nanoAgda70.01A toy dependently-typed language (dependent-types, program)2012-03-201.0.0JeanPhilippeBernardy
open-typerep270.02Open type representations and dynamic types (bsd3, dependent-types, library)2016-05-270.6.1EmilAxelsson
parameterized-utils872.06Classes and data structures for working with data-kind indexed types (bsd3, data-structures, dependent-types, library)2024-01-152.1.8.0KevinQuick, RobertDockins, ryanglscott, galoisinc
path-sing40.00A singleton wrapper for the `path` library. (dependent-types, filesystem, library, mpl, system)2023-09-180.1.0.0YamadaRyo
pisigma130.01A dependently typed core language (bsd3, dependent-types, development, language, library, program)2011-05-180.2.1AndresLoeh, DarinMorrison
prim-uniq610.04Opaque unique identifiers in primitive state monads (data, dependent-types, library, public-domain)2020-04-150.2BertramFelgenhauer, JamesCook, RyanTrinkle
proof-assistant-bot130.00Telegram bot for proof assistants (dependent-types, library, mit, program)2024-02-070.2.2swamp_agr
ral1630.04Random access lists (data, dependent-types, gpl, library, singletons)2022-01-030.2.1phadej
ral-lens100.00Length-indexed random access lists: lens utilities. (data, dependent-types, gpl, lens, library, singletons)2021-02-280.2phadej
ral-optics90.00Length-indexed random access lists: optics utilities. (data, dependent-types, gpl, library, optics, singletons)2021-02-280.2phadej
reflection3772.2592Reifies arbitrary terms into types that can be reflected back into terms (bsd3, data, dependent-types, library, reflection)2023-02-282.1.7EdwardKmett, ryanglscott
rzk882.01An experimental proof assistant for synthetic ∞-categories (bsd3, dependent-types, library, program)2024-04-020.7.4NickolayKudasov
show-type100.04convert types into string values in haskell (bsd3, dependent-types, library)2015-01-080.1.1Kinokkory
singleton-dict40.01Typelevel balanced search trees via a singletonized Data.Map (bsd3, data, dependent-types, library)2017-06-090.1.0.0ArieMiddelkoop
singleton-nats560.02Unary natural numbers relying on the singletons infrastructure. (bsd3, data, dependent-types, library)2023-10-130.4.7AndrasKovacs, ryanglscott
singletons1782.75120Basic singleton types and definitions (bsd3, dependent-types, library)2022-08-233.0.2RichardEisenberg, ryanglscott
singletons-base1000.023A promoted and singled version of the base library (bsd3, dependent-types, library)2023-10-133.3ryanglscott
singletons-th1140.08A framework for generating singleton types (bsd3, dependent-types, library)2023-10-133.3ryanglscott
some4350.025Existential type: Some (bsd3, data, dependent-types, library)2023-10-241.0.6phadej
symbols320.03Symbol manipulation (bsd3, dependent-types, library)2019-09-100.3.0.0kcsongor
tensor-safe52.00Create valid deep neural network architectures (ai, bsd3, dependent-types, language, library, program)2019-05-030.1.0.1leopiney
type-equality1940.014Data.Type.Equality compat package (bsd3, data, dependent-types, library)2019-09-061ErikHesselink, phadej, ryanglscott
type-fun270.05Collection of widely reimplemented type families (bsd3, dependent-types, library)2021-06-040.1.3AlekseyUymanov
type-level-bst30.01type-level binary search trees in haskell (bsd3, data-structures, dependent-types, library)2014-10-280.1Kinokkory
typeparams170.01Lens-like interface for type level parameters; allows unboxed unboxed vectors and supercompilation (bsd3, configuration, data, dependent-types, library, optimization)2015-01-260.0.6MikeIzbicki
uAgda190.01A simplistic dependently-typed language with parametricity. (dependent-types, program)2012-03-101.2.0.4JeanPhilippeBernardy
vec450.05Vec: length-indexed (sized) list (bsd3, data, dependent-types, library)2023-03-210.5phadej
vec-lens100.00Vec: length-indexed (sized) list: lens support (bsd3, data, dependent-types, lens, library)2021-02-280.4phadej
vec-optics120.00Vec: length-indexed (sized) list: optics support (bsd3, data, dependent-types, library, optics)2021-02-280.4phadej