-
Samizdat Public
being bits and pieces I'm inclined to leave lying around
-
Syrup Public
being a programming language for sequential circuits
-
TypesWhoSayNi Public
being the materials for a paper I have in mind to write about the bidirectional discipline
-
MS4P Public
being some thoughts about introductory mathematics for computer science
-
-
leibniz Public
being a toy which invites its user to evaluate applicative Haskell programs
-
-
-
ask-bis Public
being a second attempt to build the ask proof assistant, hopefully with less flake
1 UpdatedOct 6, 2022 -
SmolCat Public
being an exploration of categories small enough for arrows to have uncontroversially intensional equality
7 UpdatedJul 15, 2022 -
EGTBS Public
being the introduction to co-de-Bruijn metasyntax
-
ProgrammerCommaCon Public
being a collection of Agda-facilitated ramblings
-
-
-
-
CS410-18 Public
being the teaching materials and exercises for CS410 in the 2018/19 session
-
-
-
-
-
-
InteriorDesign Public
being the monadic treatment of interiors indexed by perimeters
-
CS410-17 Public
being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde
-
Saturday Public
being a thing I build on a Saturday
-
-
Bi71 Public
being a bidirectional reformulation of Martin-Löf's 1971 type theory
-
Ohrid-Agda Public
being my notes and exercises for the Types Summer School in Ohrid, (FYRO) Macedonia, July 2017
-
-
Pert Public
being some thoughts about the succinct organisation of data by pertinence
UpdatedMay 14, 2017 -
CS410-16 Public
being the lecture materials and exercises for the 2016/17 session of Advanced Functional Programming at Strathclyde