Pinned Repositories
cat
Formalizing Category Theory in Agda using Cubical Type Theory
cubical-demo
guarded-exp
Experiments with models of "guarded recursion"
hereditary
Hereditary Substitution
hottest-talk
ITT9200
ITT9200 - A reading group on "Syntax and Semantics of Dependent Types" by Martin Hofmann
miller
Miller/pattern unification in Agda
parametric-demo
Saizan's Repositories
Saizan/cubical-demo
Saizan/parametric-demo
Saizan/hottest-talk
Saizan/cat
Formalizing Category Theory in Agda using Cubical Type Theory
Saizan/guarded-exp
Experiments with models of "guarded recursion"
Saizan/agda
Agda is a dependently typed programming language / interactive theorem prover.
Saizan/Agda-proofs
Agda code for the proofs I use in my research
Saizan/agda-stdlib
The Agda standard library
Saizan/AgdaProofs
My agda proofs for my internship at Chalmers with Mr. Coquand
Saizan/agdarsec
Total Parser Combinators in Agda
Saizan/awesome-plutus
Saizan/chi
Saizan/classical-bp
Approximation Alg. for Classical Bin Packing
Saizan/closed-canonicity
Some Agda code with the intent to formalize a proof of canonicity for type theory
Saizan/cubical-1
Saizan/cubicaltt
Saizan/dependent-lenses
Saizan/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
Saizan/inductive_types
Saizan/io-sim
Haskell's IO simulator which closely follows core packages (base, async, stm).
Saizan/lambda-definability
Lambda-definability and NBE for simply-typed lambda-calculus and maybe beyond
Saizan/letter
Saizan/openai-hs
Unofficial OpenAI Haskell Bindings
Saizan/openapi3
OpenAPI 3.0 data model
Saizan/pdtt
Saizan/platypus
Saizan/plutarch-plutus
Typed eDSL for writing UPLC /ˈpluː.tɑːk/
Saizan/Saizan.github.io
Saizan/syb-with-class
Fork of http://patch-tag.com/r/Saizan/syb-with-class
Saizan/thesis