Formal proofs for modal calculi in Agda.

I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies.

A tracker for misogyny issues in tech

The Agda standard library

Parametric Fitch-style modal lambda calculus

A repository for material from the reading group on NbE

A description of me!

audible feedback on just how much your browsing feeds into google

Algebraic proof discovery in Agda

The best way to write secure and reliable applications. Write nothing; deploy nowhere.

Agda formalisation of second-order abstract syntax

Normalization by evaluation of simply typed combinators.

An extension of the NbE algorithm to produce computational traces

This aims to be the most pretentious implementation of stlc in existence

A self-contained repository for the paper Type and Scope Preserving Semantics

ETC

Formalizing nbe in agda

Supporting Material for the paper "Embedding-By-Normalisation"

Women in Programming Languages and Software Engineering Research

Library of the ##dependent distributed research support group

Agda formalisation of NbE for λ□

Experiments with modal types

Agda formalisation of dual-context constructive modal logics.

Formal Topology in Univalent Foundations (WIP).

Set of utility functions to facilitate working with language-c99

Implementation of C99's AST and pretty printer in Haskell, strictly following www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf

Simplified C AST that translates to language-c99