There are no reviews yet. Be the first to send feedback to the community and the maintainers!
learn-tt
A collection of resources for learning type theory and type theory adjacent fields.higher-order-unification
A small implementation of higher-order unificationpcf
A small compiler for PCFblott
An experimental type checker for a modal dependent type theory.nbe-for-mltt
Normalization by Evaluation for Martin-Lรถf Type Theoryhm
A small implementation of type inferenceminiprl
A small implementation of a proof refinement logic.wiki-summary.el
Get summaries of wikipedia articles in Emacsundergraduate-thesis
A discouraging story.graph-models
Notes on P-omegamodal
Modal logic in Haskell through Static Pointerssml-fingertree
The ugliness is worth it, the ugliness is worth it, the ugliness...cooked-pi
What if we built the same frustrating type checker over and over again? For science.independence-of-the-continuum-hypothesis
Some notes on the independence of the continuum hypothesis.c-dsl
a dsl for generating Cregister-alloc
WIP - A little doodle of a register allocator with an explanation of how it works.fibrational-semantics
Notes on simple fibrational semantics.hlf
an implementation of LFhi
A toy interpreter for Haskellsml-kanren
Let's make another miniKanren.concurrent-stack-with-helping
A case study in Iris formalizing a concurrent stack with helping.ds-kanren
a tiny logic programming languageemacs.d
my emacs configsecret-notes
Containing small notes which aren't original or noteworthy, but which I don't want to lose.hasquito
a dysfunctional compiler to javascriptsml-abt-unify
Simple unification for ABTs in SMLblog
the source for jozefg.bitbucket.orga-short-talk-on-iris
The notes for a short talk given on Iris in a seminar on concurrent separation logic at Carnegie Mellon.bound-gen
Making bound play nice with monad-gen.regex
an exercise in decision procedures in Agdafolds-common
A conglomeration of folds.ctt.elf
Probably wrong formalization of computational type theory in Twelf.drafts
Drafts of posts for my blogkripke
Modal logic and Kripke semantics in Twelfoplss
My notes from OPLSS and related pre-lecture-thingieshotc
Notes on higher-order typed compilation. Probably wrongsml-higher-order-matching
A (probably broken) second order pattern matchingsimple-abt
Nothing fancy, just binding without paingeneric-church
automatic church encodingsmonad-gen
a monad for fresh valuesf2js
A compiler in need of a better namejozefg.github.io
websitereified-records
automatic reification of records to mapsc_of_scheme
a lousy scheme compilerLove Open Source and this site? Check out how you can help us