jonsterling Goto Github PK

category-theory

A formalization of category theory in Coq for personal study and practical work

ccg-framework

A framework for testing multi-modal CCG constructions

ccg-paper

The type-theoretic definition of multimodal CCG. Written in informal type theory, proved in Agda.

choice-sequences

chtt-s18-lecture-notes

cmlib

A basic library of algorithms and data structures (a la NJlib)

color-editor

Example purescript-halogen application.

commercialhaskell

A special interest group for companies and individuals interested in commercial usage of Haskell

constrain

Responsive, animated figures in JavaScript/HTML canvases

constructive-sheaf-semantics

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

contracsrankings

Exposing the dangers of metric-based scientific rankings

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-algebra

coq-algebra-experiments

Formalizing some basic commutative algebra in Coq in order to procrastinate on my thesis proposal and paper reviews.

coq-cbpv

coq-domains

coq-guarded-computational-type-theory

coq-meaning-explanation

coq-presheaf-cwf

coq-sgdt

coq-synthetic-realizability

Some experiments

coq-up

A tarpit in Coq

cubical

Implementation of Univalence in Cubical Sets

cubical-1

cubicalexperiments

HoTT MRC Cubical experiments group

diaconescu-tt

An Agda proof of Diaconescu's Theorem for Constructive Type Theory using Setoids

dingle-dangle

The Dingle-Dangle NL syntax formalism. The normalization bit is cribbed from various places.

dingle-dangle-agda-old

docco

Literate Programming can be Quick and Dirty.

drafts

Drafts of posts for my blog