daniel gratzer

modal. Modal logic in Haskell through Static Pointers

9

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

8

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

8

c-dsl. a dsl for generating C

7

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

7

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

6

fibrational-semantics. Notes on simple fibrational semantics.

6

sml-kanren. Let's make another miniKanren.

5

hlf. an implementation of LF

5

ds-kanren. a tiny logic programming language

4

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

4

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

4

hi. A toy interpreter for Haskell

4

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

3

blog. the source for jozefg.bitbucket.org

3

emacs.d. my emacs config

3

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

3

c_of_scheme. a lousy scheme compiler

2

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

2

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

2

drafts. Drafts of posts for my blog

2

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

2

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

2

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

2

folds-common. A conglomeration of folds.

2

monad-gen. a monad for fresh values

2

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

2

kripke. Modal logic and Kripke semantics in Twelf

2

simple-abt. Nothing fancy, just binding without pain

2

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

2

generic-church. automatic church encodings

2

regex. an exercise in decision procedures in Agda

2

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

2

hasquito. a dysfunctional compiler to javascript

2

reified-records. automatic reification of records to maps

1

iris-project. HTML

1

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

1

jozefg.github.io. website

1

f2js. A compiler in need of a better name

1