Pinned Repositories
Big-step-Normalisation
Agda formalisations of some big-step normalization proofs
categories
A category theory library for Agda
Go-Tour
ITT8060
ITT9200
ITT9200 - A reading group on "Syntax and Semantics of Dependent Types" by Martin Hofmann
Number-Theory
Currently this repo contains a translation of Thierry Coquands proof of the irrationality of 2 from agda 1 to agda 2
Relative-Monads
Relative Monad Library for Agda
restriction-categories
A formalisation of Restriction Categories in Agda
TT-in-TT
Type theory in type theory
jmchapman's Repositories
jmchapman/Relative-Monads
Relative Monad Library for Agda
jmchapman/Big-step-Normalisation
Agda formalisations of some big-step normalization proofs
jmchapman/restriction-categories
A formalisation of Restriction Categories in Agda
jmchapman/categories
A category theory library for Agda
jmchapman/ITT9200
ITT9200 - A reading group on "Syntax and Semantics of Dependent Types" by Martin Hofmann
jmchapman/Number-Theory
Currently this repo contains a translation of Thierry Coquands proof of the irrationality of 2 from agda 1 to agda 2
jmchapman/Go-Tour
jmchapman/ITT8060
jmchapman/agda
Agda is a dependently typed programming language / interactive theorem prover.
jmchapman/agda-logos
Aive Kalmus's agda logo designs
jmchapman/agda-stdlib
The Agda standard library
jmchapman/agda2hs
Compiling Agda code to readable Haskell
jmchapman/agda2rust
jmchapman/agda_rust_interop
jmchapman/cardano-updates
jmchapman/CS410-17
being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde
jmchapman/Foogle.Charts
Easy to use F# wrapper for Google Charts visualization library
jmchapman/fsharp.github.io
F# GitHub Community Webpages
jmchapman/generic-syntax
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
jmchapman/itt8060-1
jmchapman/ITT8060.2013
ITT8060 Advanced Programming
jmchapman/jmchapman.github.io
website
jmchapman/lambda-calculus
Formalisation of normalisation by evaluation for simply typed lambda calculus extended with natural numbers, lists, pairs, and streams.
jmchapman/levlam
jmchapman/LibAgda
jmchapman/MSPweb
being the shared sources and generated html for the MSP website
jmchapman/plfa.github.io
Introduction to programming language theory in Agda.
jmchapman/plutus
The Plutus language implementation and tools
jmchapman/smoera
jmchapman/utxo