Pinned Repositories
aether-app
Aether client app with bundled front-end and P2P back-end
catala
Programming language for literate programming law specification
crd
Computing the Cohomology of Root Data
cwa-app-ios
Native iOS app using the exposure notification framework from Apple.
hott-book
Solutions of the exercises of the book "Homotopy Type Theory", a.k.a. "the HoTT book".
paper-wallet
Tool for generating PDF print templates of paper wallets for Monero.
PGL2Z
An implementation of the projective linear group of 2x2 matrices over the integers (extended modular group) as a Coxeter group in Sage.
tapl
Solutions to the exercises in and miscellaneous material for the book "Types and Programming Languages" by Benjamin C. Pierce.
tdd
Solutions to the exercises in 'Type-Driven Development with Idris'
mr-infty's Repositories
mr-infty/tapl
Solutions to the exercises in and miscellaneous material for the book "Types and Programming Languages" by Benjamin C. Pierce.
mr-infty/PGL2Z
An implementation of the projective linear group of 2x2 matrices over the integers (extended modular group) as a Coxeter group in Sage.
mr-infty/aether-app
Aether client app with bundled front-end and P2P back-end
mr-infty/catala
Programming language for literate programming law specification
mr-infty/crd
Computing the Cohomology of Root Data
mr-infty/cwa-app-ios
Native iOS app using the exposure notification framework from Apple.
mr-infty/hott-book
Solutions of the exercises of the book "Homotopy Type Theory", a.k.a. "the HoTT book".
mr-infty/paper-wallet
Tool for generating PDF print templates of paper wallets for Monero.
mr-infty/tdd
Solutions to the exercises in 'Type-Driven Development with Idris'
mr-infty/eschalot
It is important to stress that we have not written this piece of software.
mr-infty/ffmpeg
mr-infty/idris-algebra
This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra"
mr-infty/idris-crypto
Implementation of cryptographic primitives using Idris
mr-infty/Idris-dev
A Dependently Typed Functional Programming Language
mr-infty/idris-lisp
An empty code generator, to be used as a starting point for any new back ends.
mr-infty/idris-vim
Idris mode for vim
mr-infty/Idris2
A purely functional programming language with first class types
mr-infty/idris2-vim
Vim mode for Idris 2
mr-infty/lean-liquid
💧 Liquid Tensor Experiment
mr-infty/learn-idris-pub
Public data for https://learn-idris.net/
mr-infty/perfectoid-spaces
A formalization of the concept of a perfectoid space in the Lean formal theorem prover.
mr-infty/sparse
A simple (toy) parser combinator library for educational purposes.
mr-infty/the-hott-book
A textbook on informal homotopy type theory.
mr-infty/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
mr-infty/us-elections2020
A statistical analysis of the election results of the general election 2020.
mr-infty/xmr-wasm
A Monero WebAssembly based miner