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
Agda4172.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)90.01Command-line program for type-checking and compiling Agda programs (dependent-types, deprecated, program)2012-03-122.3.0.1NilsAndersDanielsson, UlfNorell
MiniAgda292.01A toy dependently typed programming language with type-based termination. (dependent-types, mit, program)2022-03-110.2022.3.11AndreasAbel
PandocAgda (deprecated)70.01Pandoc support for literate Agda (bsd3, dependent-types, deprecated, library, program)2013-03-112.3.3.0.2PeterDivianszky
Sit220.01Prototypical type checker for Type Theory with Sized Natural Numbers (dependent-types, library, program)2023-08-030.2023.8.3AndreasAbel
aeson-dependent-sum40.00JSON encoding/decoding for dependent-sum (data, dependent-types, gpl, json, library)2022-08-270.1.0.1jack
agda-server (deprecated)90.01Http server for Agda (prototype) (bsd3, dependent-types, deprecated, program)2013-10-030.1.1PeterDivianszky
agda-snippets (deprecated in favor of Agda)100.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)110.01Literate Agda support using agda-snippets, for Hakyll pages. (bsd3, dependent-types, deprecated, library)2017-06-040.1.2.2LiamOConnorDavis
agda-unused100.00Check for unused code in an Agda project. (dependent-types, library, mit, program)2022-11-260.3.0msuperdock
agda2lagda250.00Translate .agda files into .lagda.tex files. (dependent-types, development, program)2023-06-090.2023.6.9AndreasAbel
bin1510.05Bin: binary natural numbers. (data, dependent-types, gpl, library, math, singletons)2023-03-210.1.3phadej
compare-type120.01compare types of any kinds in haskell (bsd3, dependent-types, library)2015-01-100.1.1Kinokkory
cubical90.01Implementation of Univalence in Cubical Sets (dependent-types, mit, program)2014-04-270.2.0AndersMortberg
dec2310.04Decidable propositions. (bsd3, data, dependent-types, library)2024-05-170.0.6phadej
decidable340.02Combinators for manipulating dependently-typed predicates. (bsd3, dependent-types, library)2024-02-280.3.1.1jle
dependent-map1572.536Dependent finite maps (partial dependent products) (data, dependent-types, library)2020-03-270.4.0.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch
dependent-sum2992.2559Dependent sum type (data, dependent-types, library, public-domain)2022-12-220.7.2.0BertramFelgenhauer, JamesCook, JohnEricson, RyanTrinkle, abrar, 3noch, DanBornside
eliminators500.01Dependently typed elimination functions using singletons (bsd3, dependent-types, library)2024-05-120.9.5ryanglscott
fin1612.012Nat and Fin: peano naturals and finite numbers (bsd3, data, dependent-types, library, math, singletons)2023-03-210.3phadej
helf120.01Typechecking terms of the Edinburgh Logical Framework (LF). (dependent-types, mit, program)2024-03-181.0.20240318AndreasAbel
hoq80.01A language based on homotopy type theory with an interval type (dependent-types, gpl, program)2014-09-270.3valis
idris2672.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)170.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
lens-typelevel60.01Type-level lenses using singletons (bsd3, dependent-types, lenses, library)2018-10-290.1.1.0jle
list-witnesses150.00Witnesses for working with type-level lists (bsd3, dependent-types, library)2024-02-280.1.4.1jle
nanoAgda60.01A toy dependently-typed language (dependent-types, program)2012-03-201.0.0JeanPhilippeBernardy
open-typerep220.02Open type representations and dynamic types (bsd3, dependent-types, library)2016-05-270.6.1EmilAxelsson
parameterized-utils822.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-sing50.00A singleton wrapper for the `path` library. (dependent-types, filesystem, library, mpl, system)2023-09-180.1.0.0YamadaRyo
pisigma80.01A dependently typed core language (bsd3, dependent-types, development, language, library, program)2011-05-180.2.1AndresLoeh, DarinMorrison
prim-uniq520.04Opaque unique identifiers in primitive state monads (data, dependent-types, library, public-domain)2020-04-150.2BertramFelgenhauer, JamesCook, RyanTrinkle
proof-assistant-bot80.00Telegram bot for proof assistants (dependent-types, library, mit, program)2024-02-070.2.2swamp_agr
ral1360.04Random access lists (data, dependent-types, gpl, library, singletons)2022-01-030.2.1phadej
ral-lens60.00Length-indexed random access lists: lens utilities. (data, dependent-types, gpl, lens, library, singletons)2021-02-280.2phadej
ral-optics80.00Length-indexed random access lists: optics utilities. (data, dependent-types, gpl, library, optics, singletons)2021-02-280.2phadej
reflection4342.2593Reifies arbitrary terms into types that can be reflected back into terms (bsd3, data, dependent-types, library, reflection)2024-05-042.1.8EdwardKmett, ryanglscott
rzk152.01An experimental proof assistant for synthetic ∞-categories (bsd3, dependent-types, library, program)2024-04-020.7.4NickolayKudasov
show-type40.04convert types into string values in haskell (bsd3, dependent-types, library)2015-01-080.1.1Kinokkory
singleton-dict20.01Typelevel balanced search trees via a singletonized Data.Map (bsd3, data, dependent-types, library)2017-06-090.1.0.0ArieMiddelkoop
singleton-nats490.02Unary natural numbers relying on the singletons infrastructure. (bsd3, data, dependent-types, library)2023-10-130.4.7AndrasKovacs, ryanglscott
singletons2082.75120Basic singleton types and definitions (bsd3, dependent-types, library)2024-05-123.0.3RichardEisenberg, ryanglscott
singletons-base940.023A promoted and singled version of the base library (bsd3, dependent-types, library)2024-05-123.4ryanglscott
singletons-th1220.08A framework for generating singleton types (bsd3, dependent-types, library)2024-05-123.4ryanglscott
some3560.028Existential type: Some (bsd3, data, dependent-types, library)2023-10-241.0.6phadej
symbols260.03Symbol manipulation (bsd3, dependent-types, library)2019-09-100.3.0.0kcsongor
tensor-safe62.00Create valid deep neural network architectures (ai, bsd3, dependent-types, language, library, program)2019-05-030.1.0.1leopiney
type-equality1710.014Data.Type.Equality compat package (bsd3, data, dependent-types, library)2024-05-121.0.1ErikHesselink, phadej, ryanglscott
type-fun240.05Collection of widely reimplemented type families (bsd3, dependent-types, library)2021-06-040.1.3AlekseyUymanov
type-level-bst60.01type-level binary search trees in haskell (bsd3, data-structures, dependent-types, library)2014-10-280.1Kinokkory
typeparams110.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
uAgda230.01A simplistic dependently-typed language with parametricity. (dependent-types, program)2012-03-101.2.0.4JeanPhilippeBernardy
vec370.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-optics80.00Vec: length-indexed (sized) list: optics support (bsd3, data, dependent-types, library, optics)2021-02-280.4phadej