Let's rethink how we interact with Agda

A semantics for our proposed design for algebraic effects for OCaml

Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]

Analytic sampler framework for algebraic data types

A Coq library for abstract syntactical reasoning

I will read and engage with one paper a week.

Formalization of C++ for verification purposes.

the file filesystem: mount semi-structured data (like JSON) as a Unix filesystem

Best of POPL (BOP) Reading Group Memoirs

MoCHi: Model Checker for Higher-Order Programs

Yes, it's true 💜

Old Clowdr versions 1 & 2 from 2020

Session Type EDSL for Rust

An HTML+CSS template for making more accessible posters

Bidirectional Parsing. Work in Progress

Mutation analysis tool for Coq verification projects

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Easily create authenticated data structures

A cryptographically verifiable code review system for the cargo (Rust) package manager.

Total functional programming (ESFP) literature

eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee

Enumeration for indexed datatypes

A collaborative bibliography of work related to the theory and practice of computational effects

💃 an applicative functor that seamlessly talks to HTML inputs

A small library and executable for generating dice rolls.

Provides an arity-generic version of the liftA2, liftA3... liftAn functions

A Super Kawaii Dependently Typed Programming Language