elpinal

elpinal's Stars

• leanprover-community/mathlib4

  The math library of Lean 4

  Language:Lean1.2k41379257

• UniMath/UniMath

  This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

  Language:Coq93356507171

• smlnj/smlnj

  Standard ML of New Jersey

  Language:Standard ML1741427713

• fizruk/rzk

  An experimental proof assistant based on a type theory for synthetic ∞-categories.

  Language:Haskell805404

• mikeshulman/catlog

  Categorical logic from a categorical point of view

  Language:TeX751319

• jonsterling/forest

  My mathematical Zettelkasten, created using forester.

  Language:Shell72454

• emilyriehl/yoneda

  comparative formalizations of the Yoneda lemma for 1-categories and infinity-categories

  Language:Lean606125

• AndrasKovacs/cctt

  high-performance cubical evaluation

  Language:TeX581113

• zydeco-lang/zydeco

  a proof-of-concept programming language based on Call-by-push-value

  Language:Rust494433

• felixwellen/synthetic-zariski

  Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

  Language:TeX4823294

• pamellies/models-of-programming-languages

  Slides and handwritten notes on the course on models of programming languages

  48100

• tomdjong/MGS-domain-theory

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

  Language:TeX44304

• AndrasKovacs/sett

  Setoid type theory implementation

  Language:Haskell38112

• mikeshulman/ohtt

  H.O.T.T. using rewriting in Agda

  Language:Agda3614123

• ecavallo/ptt

  Experimental type-checker for internally parametric type theory

  Language:OCaml32800

• uemurax/hott-ja

  HoTT in Japanese

  Language:Racket32231

• RedPRL/algaett

  🦠 An experimental elaborator for dependent type theory using effects and handlers

  Language:OCaml307150

• AndrasKovacs/universes

  Generalized syntax & semantics for universe hierarchies

  Language:TeX2860

• logsem/mitten_preorder

  Language:OCaml26611

• plt-amy/cubical-methods

  A textbook on cubical type theory

  Language:TeX220

• marcinjangrzybowski/cubeViz2

  Language:Haskell212

• uemurax/morg

  Organize mathematical thoughts

  Language:Racket18311

• AndrasKovacs/preordertt

  Experiments with preordered set models of (directed) type theories

  Language:Agda151

• smimram/catt

  An infinity-categorical coherence typechecker

  Language:OCaml15400

• ericfinster/catt

  Coherence typechecker for Grothendieck/Maltsiniotis style infinity categories

  Language:Haskell13401

• cchanavat/lean-topos

  Some topos theory in Lean

  Language:Lean10

• maxsnew/cubical-cbpv

  A Formalization of Internal CBPV Models in Cubical Agda

  Language:Agda8200

• kbuzzard/etale_experiments

  Experiments with definition of etale morphisms etc

  Language:Lean5101

• j-emmen/W-types-in-setoids

  This is the Coq formalisation of the paper "W-types in setoids", arXiv:1809.02375.

  Language:Coq4

• paolobrasolin/quantales

  Language:Agda350