mortberg

Sweden

Pinned Repositories

agda
Agda is a dependently typed programming language / interactive theorem prover.
Language:Haskell0 2 00
AlgTop
Haskell library of algebraic topology
Language:Haskell23 3 01
bnfc
BNF Converter
Language:TeX0 2 00
cubeval
high-performance cubical evaluation
Language:TeX0 1 00
cubicaltt
Experimental implementation of Cubical Type Theory
Language:Haskell572 45 6176
gen-cart
A Unifying Cartesian Cubical Set Model
Language:Agda33 5 01
martin-lof
papers of Per Martin Löf
Language:TeX3 2 01
Schools
Language:Coq1 2 00
TypeTheory
Language:Coq7 4 01
yacctt
yacctt: Yet Another Cartesian Cubical Type Theory
Language:Haskell74 12 28

mortberg's Repositories

mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
Language:Haskell572 45 6176
mortberg/yacctt
yacctt: Yet Another Cartesian Cubical Type Theory
Language:Haskell74 12 28
mortberg/gen-cart
A Unifying Cartesian Cubical Set Model
Language:Agda33 5 01
mortberg/AlgTop
Haskell library of algebraic topology
Language:Haskell23 3 01
mortberg/TypeTheory
Language:Coq7 4 01
mortberg/martin-lof
papers of Per Martin Löf
Language:TeX3 2 01
mortberg/Schools
Language:Coq1 2 00
mortberg/agda
Agda is a dependently typed programming language / interactive theorem prover.
Language:Haskell0 2 00
mortberg/bnfc
BNF Converter
Language:TeX0 2 00
mortberg/cubeval
high-performance cubical evaluation
Language:TeX0 1 00
mortberg/cubical
Language:Agda0 2 00
mortberg/cubical-demo
Language:Agda0 2 00
mortberg/europroofnet.github.io
Sources of the EuroProofNet web site.
Language:Ruby1 0
mortberg/HoTT
Homotopy type theory
Language:Coq2 0
mortberg/OEIS-A000001
Language:Agda1 0
mortberg/palmgren-archive
Research material of Erik Palmgren (1963–2019)
Language:Agda1 0
mortberg/sml-redprl
Decisively Smash the Formalist Clique!—The People's Refinement Logic
Language:Standard ML2 0
mortberg/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Language:Coq3 0