Jesper Cockx

agda-lecture-notes. Agda lecture notes for the Functional Programming course at TU Delft

agda-core. A work-in-progress core language for Agda, in Agda

ataca. A TACtic library for Agda

agda2scheme. Compiler backend for generating Scheme code

popl19-tutorial. Files for the tutorial "Correct-by-construction programming in Agda" at POPL '19 in Cascais

ohrid19-agda. Material for the Agda course at the EUTYPES Summer School '19 in Ohrid

reflection-tutorial. 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.

scope. An agda2hs-compatible library for well-scoped syntax

ttac. Typed functional-style tactics for Agda

telescopic. Agda

tensors. Some experiments with defining tensors in Agda

lbss-lecture-notes. Lecture notes for CSE4280 Language-Based Software Security at TU Delft

scopes-n-roses. What's in a scope? An abstract representation of scopes in Agda.

lagda-slides-template. A template for creating Beamer slides with literate Agda code

revealjs-agda-template. A quick template for creating Agda slides with Reveal.js

categories. There are many definitions of categories in Agda, but this one is mine.

nano_photos_provider2. PHP photos provider for nanogallery2

Weblab-Haskell. Haskell test runner for Weblab

website. Hakyll code for building my website at jesper.sikanda.be

agda2hs. Compiling Agda code to readable Haskell

generics. Agda

pubnotes. My published notes

Weblab-Agda. Agda support for Weblab

pi-forall. A demo implementation of a simple dependently-typed language

book. A textbook on informal homotopy type theory

agda. Agda is a dependently typed programming language / interactive theorem prover.