Packages tagged dependent-types

54 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (44), bsd3 (34), data (19), program (18), gpl (6), mit (5), singletons (5), deprecated (4), data-structures (2), development (2), language (2), lens (2), math (2), optics (2), public-domain (2), ...

Name
DLs
Rating
Rev Deps
Description
Tags
Last U/L
Last Version
Maintainers
Agda4712.758A dependently typed functional programming language and proof assistant (dependent-types, program)2023-01-302.6.2.2AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell
Agda-executable (deprecated in favor of Agda)100.01Command-line program for type-checking and compiling Agda programs (dependent-types, deprecated, program)2012-03-122.3.0.1NilsAndersDanielsson, UlfNorell
MiniAgda182.01A toy dependently typed programming language with type-based termination. (dependent-types, mit, program)2022-03-110.2022.3.11AndreasAbel
PandocAgda60.01Pandoc support for literate Agda (bsd3, dependent-types, library, program)2013-03-112.3.3.0.2PeterDivianszky
Sit150.01Prototypical type checker for Type Theory with Sized Natural Numbers (dependent-types, library, program)2022-03-180.2022.3.18AndreasAbel
aeson-dependent-sum30.00JSON encoding/decoding for dependent-sum (data, dependent-types, gpl, json, library)2022-08-270.1.0.1jack
agda-server110.01Http server for Agda (prototype) (bsd3, dependent-types, program)2013-10-030.1.1PeterDivianszky
agda-snippets (deprecated in favor of Agda)90.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)60.01Literate Agda support using agda-snippets, for Hakyll pages. (bsd3, dependent-types, deprecated, library)2017-06-040.1.2.2LiamOConnorDavis
agda-unused90.00Check for unused code in an Agda project. (dependent-types, library, mit, program)2022-11-260.3.0msuperdock
agda2lagda240.00Translate .agda files into .lagda.tex files. (dependent-types, development, program)2023-03-250.2021.6.1AndreasAbel
bin2340.05Bin: binary natural numbers. (data, dependent-types, gpl, library, math, singletons)2023-03-210.1.2phadej
compare-type20.01compare types of any kinds in haskell (bsd3, dependent-types, library)2015-01-100.1.1Kinokkory
cubical50.01Implementation of Univalence in Cubical Sets (dependent-types, mit, program)2014-04-270.2.0AndersMortberg
dec2940.04Decidable propositions. (bsd3, data, dependent-types, library)2022-08-210.0.5phadej
decidable150.02Combinators for manipulating dependently-typed predicates. (bsd3, dependent-types, library)2020-02-030.3.0.0jle
dependent-map2032.531Dependent finite maps (partial dependent products) (data, dependent-types, library)2020-03-270.4.0.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch
dependent-sum4942.2555Dependent sum type (data, dependent-types, library, public-domain)2022-12-220.7.2.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch, DanBornside
eliminators580.01Dependently typed elimination functions using singletons (bsd3, dependent-types, library)2023-03-120.9.1ryanglscott
fin2622.012Nat and Fin: peano naturals and finite numbers (bsd3, data, dependent-types, library, math, singletons)2023-03-210.2.1phadej
helf100.01Typechecking terms of the Edinburgh Logical Framework (LF). (dependent-types, mit, program)2022-05-300.2022.5.30AndreasAbel
hoq40.01A language based on homotopy type theory with an interval type (dependent-types, gpl, program)2014-09-270.3valis
idris1162.251Functional Programming Language with Dependent Types (bsd3, compilers-interpreters, dependent-types, library, program)2021-10-221.3.4EdwinBrady, niklasl
instance-map20.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)100.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
lens-typelevel30.01Type-level lenses using singletons (bsd3, dependent-types, lenses, library)2018-10-290.1.1.0jle
list-witnesses130.00Witnesses for working with type-level lists (bsd3, dependent-types, library)2019-08-260.1.3.2jle
nanoAgda40.01A toy dependently-typed language (dependent-types, program)2012-03-201.0.0JeanPhilippeBernardy
open-typerep120.02Open type representations and dynamic types (bsd3, dependent-types, library)2016-05-270.6.1EmilAxelsson
parameterized-utils1572.06Classes and data structures for working with data-kind indexed types (bsd3, data-structures, dependent-types, library)2022-12-212.1.6.0KevinQuick, RobertDockins, ryanglscott, galoisinc
pisigma100.01A dependently typed core language (bsd3, dependent-types, development, language, library, program)2011-05-180.2.1AndresLoeh, DarinMorrison
prim-uniq680.04Opaque unique identifiers in primitive state monads (data, dependent-types, library, public-domain)2020-04-150.2BertramFelgenhauer, JamesCook, RyanTrinkle
proof-assistant-bot60.00Telegram bot for proof assistants (dependent-types, library, mit, program)2023-02-070.2.0swamp_agr
ral2170.04Random access lists (data, dependent-types, gpl, library, singletons)2022-01-030.2.1phadej
ral-lens150.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
reflection4972.2590Reifies arbitrary terms into types that can be reflected back into terms (bsd3, data, dependent-types, library, reflection)2023-02-282.1.6EdwardKmett, ryanglscott
show-type50.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-nats420.02Unary natural numbers relying on the singletons infrastructure. (bsd3, data, dependent-types, library)2021-03-120.4.6AndrasKovacs, ryanglscott
singletons3042.75116Basic singleton types and definitions (bsd3, dependent-types, library)2022-08-233.0.2RichardEisenberg, ryanglscott
singletons-base1500.013A promoted and singled version of the base library (bsd3, dependent-types, library)2023-03-123.1.1ryanglscott
singletons-th1540.08A framework for generating singleton types (bsd3, dependent-types, library)2023-03-123.1.1ryanglscott
some6470.023Existential type: Some (bsd3, data, dependent-types, library)2023-03-151.0.4.1RyanTrinkle, phadej
symbols400.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-equality1910.014Data.Type.Equality compat package (bsd3, data, dependent-types, library)2019-09-061ErikHesselink, phadej, ryanglscott
type-fun300.05Collection of widely reimplemented type families (bsd3, dependent-types, library)2021-06-040.1.3AlekseyUymanov
type-level-bst40.01type-level binary search trees in haskell (bsd3, data-structures, dependent-types, library)2014-10-280.1Kinokkory
typeparams130.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
uAgda100.01A simplistic dependently-typed language with parametricity. (dependent-types, program)2012-03-101.2.0.4JeanPhilippeBernardy
vec560.05Vec: length-indexed (sized) list (bsd3, data, dependent-types, library)2023-03-210.4.1phadej
vec-lens170.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