Rocqet proof language

ntype cafe summer school resources

Contributions to Microsoft's Checked C project developed by PLUMmers

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

RowScript programming language, making a better browser world

Website for RowScript

Building A Correct-By-Construction Proof Checkers For Type Theories

A Library for Representing Recursive and Impure Programs in Coq

Checked C is an extension to C that lets programmers write C code with bounds checking and improved type-safety. The goal is to let people easily make their existing C code type-safe and eliminate …

A formalization of properties of a simple imperative, memory-safe language.

Fix X/Twitter and Bluesky embeds! Use multiple images, videos, polls, translations and more on Discord, Telegram and others

Compile and run Constraint Handling Rules (CHR) in JavaScript

Conference on Homotopy Type Theory 2023

History of type theory (Chinese).

A Mastodon, Twitter, and Instagram Cross-poster

My PhD thesis.

Set up a specific version of Agda for your GitHub Actions workflow.

A mechanisation of Wasm in Rocq

Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories

An extension of the NbE algorithm to produce computational traces

🔮 A lightweight comments widget built on GitHub issues

Setoid type theory implementation

Benchmarking various normalization algorithms for the lambda calculus

Hacking synthetic Tait computability into Agda. Example: canonicity for MLTT.