Packages tagged dependent-types

55 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (45), bsd3 (35), data (19), program (19), 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
Agda2912.758A dependently typed functional programming language and proof assistant (dependent-types, program)2023-01-302.6.3AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell
Agda-executable (deprecated in favor of Agda)120.01Command-line program for type-checking and compiling Agda programs (dependent-types, deprecated, program)2012-03-122.3.0.1NilsAndersDanielsson, UlfNorell
MiniAgda192.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
Sit110.01Prototypical type checker for Type Theory with Sized Natural Numbers (dependent-types, library, program)2022-03-180.2022.3.18AndreasAbel
aeson-dependent-sum50.00JSON encoding/decoding for dependent-sum (data, dependent-types, gpl, json, library)2022-08-270.1.0.1jack
agda-server80.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)150.01Literate Agda support using agda-snippets, for Hakyll pages. (bsd3, dependent-types, deprecated, library)2017-06-040.1.2.2LiamOConnorDavis
agda-unused60.00Check for unused code in an Agda project. (dependent-types, library, mit, program)2022-11-260.3.0msuperdock
agda2lagda100.00Translate .agda files into .lagda.tex files. (dependent-types, development, program)2023-03-250.2023.3.25AndreasAbel
bin2850.05Bin: binary natural numbers. (data, dependent-types, gpl, library, math, singletons)2023-03-210.1.3phadej
compare-type60.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
dec2260.04Decidable propositions. (bsd3, data, dependent-types, library)2022-08-210.0.5phadej
decidable140.02Combinators for manipulating dependently-typed predicates. (bsd3, dependent-types, library)2020-02-030.3.0.0jle
dependent-map1592.534Dependent finite maps (partial dependent products) (data, dependent-types, library)2020-03-270.4.0.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch
dependent-sum3992.2558Dependent sum type (data, dependent-types, library, public-domain)2022-12-220.7.2.0BertramFelgenhauer, JamesCook, RyanTrinkle, abrar, 3noch, DanBornside
eliminators250.01Dependently typed elimination functions using singletons (bsd3, dependent-types, library)2023-03-120.9.3ryanglscott
fin3032.012Nat and Fin: peano naturals and finite numbers (bsd3, data, dependent-types, library, math, singletons)2023-03-210.3phadej
helf80.01Typechecking terms of the Edinburgh Logical Framework (LF). (dependent-types, mit, program)2022-05-300.2022.5.30AndreasAbel
hoq70.01A language based on homotopy type theory with an interval type (dependent-types, gpl, program)2014-09-270.3valis
idris1042.251Functional Programming Language with Dependent Types (bsd3, compilers-interpreters, dependent-types, library, program)2021-10-221.3.4EdwinBrady, niklasl
instance-map60.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)130.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
lens-typelevel90.01Type-level lenses using singletons (bsd3, dependent-types, lenses, library)2018-10-290.1.1.0jle
list-witnesses110.00Witnesses for working with type-level lists (bsd3, dependent-types, library)2019-08-260.1.3.2jle
nanoAgda60.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-utils652.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
pisigma120.01A dependently typed core language (bsd3, dependent-types, development, language, library, program)2011-05-180.2.1AndresLoeh, DarinMorrison
prim-uniq600.04Opaque unique identifiers in primitive state monads (data, dependent-types, library, public-domain)2020-04-150.2BertramFelgenhauer, JamesCook, RyanTrinkle
proof-assistant-bot50.00Telegram bot for proof assistants (dependent-types, library, mit, program)2023-02-070.2.1swamp_agr
ral2450.04Random access lists (data, dependent-types, gpl, library, singletons)2022-01-030.2.1phadej
ral-lens50.00Length-indexed random access lists: lens utilities. (data, dependent-types, gpl, lens, library, singletons)2021-02-280.2phadej
ral-optics40.00Length-indexed random access lists: optics utilities. (data, dependent-types, gpl, library, optics, singletons)2021-02-280.2phadej
reflection3632.2590Reifies arbitrary terms into types that can be reflected back into terms (bsd3, data, dependent-types, library, reflection)2023-02-282.1.7EdwardKmett, ryanglscott
rzk310.01An experimental proof assistant for synthetic ∞-categories (bsd3, dependent-types, library, program)2023-05-180.4.0NickolayKudasov
show-type50.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-nats260.02Unary natural numbers relying on the singletons infrastructure. (bsd3, data, dependent-types, library)2021-03-120.4.6AndrasKovacs, ryanglscott
singletons1932.75118Basic singleton types and definitions (bsd3, dependent-types, library)2022-08-233.0.2RichardEisenberg, ryanglscott
singletons-base1210.014A promoted and singled version of the base library (bsd3, dependent-types, library)2023-03-123.2ryanglscott
singletons-th1370.08A framework for generating singleton types (bsd3, dependent-types, library)2023-03-123.2ryanglscott
some5710.024Existential type: Some (bsd3, data, dependent-types, library)2023-03-151.0.5RyanTrinkle, phadej
symbols260.03Symbol manipulation (bsd3, dependent-types, library)2019-09-100.3.0.0kcsongor
tensor-safe42.00Create valid deep neural network architectures (ai, bsd3, dependent-types, language, library, program)2019-05-030.1.0.1leopiney
type-equality1860.014Data.Type.Equality compat package (bsd3, data, dependent-types, library)2019-09-061ErikHesselink, phadej, ryanglscott
type-fun150.05Collection of widely reimplemented type families (bsd3, dependent-types, library)2021-06-040.1.3AlekseyUymanov
type-level-bst70.01type-level binary search trees in haskell (bsd3, data-structures, dependent-types, library)2014-10-280.1Kinokkory
typeparams120.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
uAgda120.01A simplistic dependently-typed language with parametricity. (dependent-types, program)2012-03-101.2.0.4JeanPhilippeBernardy
vec430.05Vec: length-indexed (sized) list (bsd3, data, dependent-types, library)2023-03-210.5phadej
vec-lens60.00Vec: length-indexed (sized) list: lens support (bsd3, data, dependent-types, lens, library)2021-02-280.4phadej
vec-optics60.00Vec: length-indexed (sized) list: optics support (bsd3, data, dependent-types, library, optics)2021-02-280.4phadej