-
elaboration-zoo Public
Minimal implementations for dependent type checking and elaboration
-
-
-
-
-
-
dtt-rtcg Public
Demo for dependent types + runtime code generation
-
singleton-nats Public
Unary natural numbers relying on the singletons infrastructure
-
www Public
Forked from teach-plt/wwwWebpages of course Programming Language Technology
Java UpdatedDec 9, 2024 -
TypeTopology Public
Forked from martinescardo/TypeTopologyLogical manifestations of topological concepts, and other things, via the univalent point of view.
Agda GNU General Public License v3.0 UpdatedAug 19, 2024 -
-
-
-
-
flat-maybe Public
Rust-style strict Maybe in Haskell: no space/indirection overhead.
-
staged-fusion Public
Staged push/pull fusion with typed Template Haskell
-
universes Public
Generalized syntax & semantics for universe hierarchies
-
smalltt Public
Demo for high-performance type theory elaboration
-
-
ghc-strict-implicit-params Public
GHC plugin for making implicit parameters strict
-
-
qiit-generalizations Public
Extending small finitary QIITs to non-small non-finitary
-
misc-stuff Public
Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.
-
aeson Public
Forked from haskell/aesonA fast Haskell JSON library
Haskell Other UpdatedMay 31, 2022 -
polynomial-model Public
A polynomial model of a Martin-Löf type theory + a bit of game semantics
-
-
StepULC Public
Forked from Bubbler-4/StepULCEfficient and single-steppable ULC evaluation algorithm
Haskell MIT License UpdatedMay 24, 2021 -
souffle-haskell Public
Forked from luc-tielen/souffle-haskellHaskell bindings for the Souffle datalog language
C++ MIT License UpdatedMay 3, 2021 -
normalization-bench Public
Lambda normalization and conversion checking benchmarks for various implementations
-
{{ message }}