Pinned Repositories
agda-core
A work-in-progress core language for Agda, in Agda
agda-lecture-notes
Agda lecture notes for the Functional Programming course at TU Delft
agda2scheme
Compiler backend for generating Scheme code
ataca
A TACtic library for Agda
cubes
An implementation of (some fragment of) cubical type theory using rewrite rules, based on a talk given by Conor McBride at the 23rd Agda's Implementor's Meeting.
ohrid19-agda
Material for the Agda course at the EUTYPES Summer School '19 in Ohrid
popl19-tutorial
Files for the tutorial "Correct-by-construction programming in Agda" at POPL '19 in Cascais
reflection-tutorial
scope
An agda2hs-compatible library for well-scoped syntax
tensors
Some experiments with defining tensors in Agda
jespercockx's Repositories
jespercockx/cubes
An implementation of (some fragment of) cubical type theory using rewrite rules, based on a talk given by Conor McBride at the 23rd Agda's Implementor's Meeting.
jespercockx/ttac
Typed functional-style tactics for Agda
jespercockx/categories
There are many definitions of categories in Agda, but this one is mine.
jespercockx/book
A textbook on informal homotopy type theory
jespercockx/pi-forall
A demo implementation of a simple dependently-typed language
jespercockx/cubical-experiments
Experiments with agda --cubical
jespercockx/higher-dimensional-syntax
Higher-dimensional syntax
jespercockx/jespercockx.github.io
jespercockx/ornaments
Some experiments based on @yoricksijsling's implementation of ornaments
jespercockx/pdtt
jespercockx/stamp