Lists (1)
Stars
A Logical Relation for Martin-Löf Type Theory in Agda
CoqHott / logrel-mltt
Forked from mr-ohman/logrel-mlttA Logical Relation for Martin-Löf Type Theory in Agda
Distributions of Agda executable compiled into WebAssembly.
Containers can be made into a Cartesian Differential Category
Formalization of the polymorphic lambda calculus and its parametricity theorem
Lecture notes and exercises for the advanced course on categorical realizability at the Midlands Graduate School (MGS) 2024
Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories
agda-web / agda
Forked from agda/agda[For generating patches for https://github.com/agda-web/agda-wasm-dist] Agda is a dependently typed programming language / interactive theorem prover.
A formalization of the theory behind the mugen library
Dynamic linking and runtime evaluation of Haskell, and C, including dependency chasing and package resolution.
josh-hs-ko / NDGP
Forked from Zekt/Type-EmbellishmentDatatype-generic programming meets elaborator reflection
An Agda formalization of System F and the Brown-Palsberg self-interpreter
👹 A library for hierarchical names and lexical scoping
Enter Unicode characters using LaTeX notation
Haskell library for space- and time-efficient operations over Unicode text.