daniel gratzer

modal. Modal logic in Haskell through Static Pointers

cooked-pi. What if we built the same frustrating type checker over and over again? For science.

sml-fingertree. The ugliness is worth it, the ugliness is worth it, the ugliness...

c-dsl. a dsl for generating C

independence-of-the-continuum-hypothesis. Some notes on the independence of the continuum hypothesis.

register-alloc. WIP - A little doodle of a register allocator with an explanation of how it works.

fibrational-semantics. Notes on simple fibrational semantics.

sml-kanren. Let's make another miniKanren.

hlf. an implementation of LF

ds-kanren. a tiny logic programming language

concurrent-stack-with-helping. A case study in Iris formalizing a concurrent stack with helping.

secret-notes. Containing small notes which aren't original or noteworthy, but which I don't want to lose.

hi. A toy interpreter for Haskell

sml-abt-unify. Simple unification for ABTs in SML

blog. the source for jozefg.bitbucket.org

emacs.d. my emacs config

classical-realizability. Notes on a realizability model for a classical logic

c_of_scheme. a lousy scheme compiler

sml-higher-order-matching. A (probably broken) second order pattern matching

JonPRL. An LCF-with-validation-style proof refinement logic based on realizability

drafts. Drafts of posts for my blog

ctt.elf. Probably wrong formalization of computational type theory in Twelf.

oplss. My notes from OPLSS and related pre-lecture-thingies

a-short-talk-on-iris. The notes for a short talk given on Iris in a seminar on concurrent separation logic at Carnegie Mellon.

folds-common. A conglomeration of folds.

monad-gen. a monad for fresh values

hotc. Notes on higher-order typed compilation. Probably wrong

kripke. Modal logic and Kripke semantics in Twelf

simple-abt. Nothing fancy, just binding without pain

effective-topos. Notes on the effective topos and related subjects.

generic-church. automatic church encodings

regex. an exercise in decision procedures in Agda

bound-gen. Making bound play nice with monad-gen.

hasquito. a dysfunctional compiler to javascript

reified-records. automatic reification of records to maps

iris-project. HTML

sml-lcf. A general purpose library for writing LCF-with-validations-style refiners

jozefg.github.io. website

f2js. A compiler in need of a better name