Jacques Carette

Drasil. Generate all the things (focusing on research software)

finally-tagless. Repo of the original work on finally tagless (and a lot of other metaocaml work besides)

TheoriesAndDataStructures. Showing how some simple mathematical theories naturally give rise to some common data-structures

pi-dual. Collaborative work on reversible computing

GenCheck. Test.GenCheck Haskell project

Notes.

panbench. System benchmarking for proof assistants

COMPSCI3MI3-F2023. Public course materials for COMPSCI 3MI3, Fall 2023 version

QuantumPi. Code repository for our work on Quantum Pi

CAS706-F2021. Repository for Fall 2021 version of CAS 706

MathScheme. Public repository for the MathScheme project

SqrtPi. Agda code accompanying the SqrtPi paper

hol-light-qe. The HOL Light theorem prover (moved from Google code)

PureBaggery. Where we explore more interesting data types than just fixed points of polynomials

Retrodictive. For exploring Symbolic Evaluation of Quantum Circuits, forwards and BACKWARDS

RetroPECode. Haskell code corresponding to the paper(s) in Retrodictive

agda-algebras. Agda

Species. Agda

Categorical-Playground. For experiments in category theory

CAS706-F2024. Public repository for CAS 706, Fall 2024 version

universal-algebra. Formalization of some universal algebra in Agda

RetrodictiveComputing. Repository for all the code that goes along with the Retrodictive Quantum Computing

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

GraphsAndTheories. Where we explore the intersection between (hyper)graphs and axiomatic theories systematically

agda-stdlib. The Agda standard library

PLGradSchools.

categories. Categories parametrized by morphism equality, in Agda

Experiments. In which I do a variety of experiments

PragmaticMetaLanguage. Working on a language that 1) encapsulates other languages, 2) integrates pragmatic concerns of languages.