-
-
-
learn-tt Public
A collection of resources for learning type theory and type theory adjacent fields.
-
nbe-for-mltt Public
Normalization by Evaluation for Martin-Löf Type Theory
-
-
wiki-summary.el Public
Get summaries of wikipedia articles in Emacs
-
-
-
-
-
secret-notes Public
Containing small notes which aren't original or noteworthy, but which I don't want to lose.
-
blott Public
An experimental type checker for a modal dependent type theory.
-
an-addendum-to-first-steps Public
A small note I wanted to keep track of on First Steps in Synthetic Guarded Domain Theory
TeX UpdatedAug 29, 2019 -
talks-for-logsem Public
slides for talks that I gave at the logic & semantics seminar at Aarhus University.
TeX UpdatedMay 24, 2019 -
Some notes on the independence of the continuum hypothesis.
-
UniMath Public
Forked from unimath2019-tt/UniMathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
-
redtt Public
Forked from RedPRL/redtt"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
OCaml Apache License 2.0 UpdatedOct 20, 2018 -
-
-
a-short-talk-on-iris Public
The notes for a short talk given on Iris in a seminar on concurrent separation logic at Carnegie Mellon.
-
cubicaltt Public
Forked from mortberg/cubicalttExperimental implementation of Cubical Type Theory
Haskell MIT License UpdatedOct 21, 2017 -
fibrational-semantics Public
Notes on simple fibrational semantics.
-
A case study in Iris formalizing a concurrent stack with helping.
-
higher-order-unification Public
A small implementation of higher-order unification
-
-
-
miniprl Public
A small implementation of a proof refinement logic.
-
sml-red-jonprl Public
Forked from RedPRL/sml-redprlThe birth of Red JonPRL.
Standard ML MIT License UpdatedJun 19, 2017 -
lawvere Public
Forked from mattearnshaw/lawvereThe collected works of F. W. Lawvere
UpdatedJan 4, 2017
{{ message }}