PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

View on GitHub

The Next 700 Module Systems

Extending Dependently-Typed Languages to Implement Module System Features In The Core Language

This repository contains the research proposal for my doctoral studies at McMaster University under the supervision of Jacques Carette and Wolfram Kahl.

What are and what should be the module systems of DTLs? DTLs remove distinctions between packaging systems and so using pedestrian modules systems is not necessarily the best route.

rather than by hand.


A super simple description of this work, for the layman, can be found here.

Prototype and a Preprint

PrototypeMathScheme: 200+ Math Theories in (Clickable) AgdaA Language Feature to Unbundle Data at WillSlidesYoutube

The Context Library ---An Agda Counterpart of the PackageFormer Prototype

PhD Thesis ; YoutubeSlides ◈ AIM 2020: Youtube; Slides


PDFHTMLSlidestranslate codemonoid codeDemo


Metaprogramming Agda — IFIP Program Generation Talk