benediktahrens Goto Github PK

birmingham-theory

The web page for the Birmingham theoretical computer science research group

book

A textbook on informal homotopy type theory

coqdoc-overlay

ct4p

euproofinfra

European e-Infrastructure on Formal Proofs

europroofnet.github.io

Sources of the EuroProofNet web site.

foundations

Development of the univalent foundations of mathematics in Coq

gruppentheorie

hlevel_n_is_of_hlevel_sn

We give a proof in Univalent Foundations that the Sigma type of types in a universe of hlevel n is itself of hlevel n+1.

hollight_experiments

Experiments in HOL Light implementing syntax and category theory

hott_cohomology

Cohomology in HoTT

ktheory

formalization of theorems of higher algebraic K-theory

largecatmodules

Large category of modules over monads on top of UniMaths and Display category

logic_and_proof

CMU Undergrad Course

logical_verification_2021

m-types

A formalization of M-types in Agda

mgs-domain-theory

Lecture notes and exercises for the introductory course on domain theory and denotational semantics at the Midlands Graduate School (MGS) 2023

milewski-ctfp-pdf

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source

monads

Coq code accompanying several articles on semantics of functional programming languages

omega_categories

Formalisation of strict omega categories and the homotopy hypothesis in type theory, using coinduction

paigenorth.github.io

rezk_completion

Rezk completion

ross-notes-2019

Ross Notes from 2019

schools

sethits

theorie-des-jeux

Course material for an introduction to game theory---in french

theory

Papers on aspects of Generalised Algebraic Theories, Contextual Categories and Mathematical Theory Of Data

triangles

Triangles

typetheory

unimath

A unified approach to formalization of mathematical knowledge based on Univalent Foundations.