NeM-T

NeM-T's Stars

• JetBrains/arend-lib

  Language:Java8023

• voodoos/ElpIDE

  Language:OCaml8

• samuelgruetter/dot-calculus

  Formalization of the Dependent Object Types (DOT) calculus

  Language:Coq639

• rafaelcgs10/W-in-Coq

  This is a Coq formalization of Damas-Milner type system and its algorithm W.

  Language:Coq251

• SRI-CSL/PVS

  The People's Verification System

  Language:Common Lisp14533

• OpenLogicProject/OpenLogic

  An open-source, customizable intermediate logic textbook

  Language:TeX1.1k249

• affeldt-aist/monae

  Monadic effects and equational reasonig in Coq

  Language:Coq7113

• protz/mezzo

  The language of the future!

  Language:OCaml7210

• imdea-software/htt

  Hoare Type Theory

  Language:Coq705

• ilyasergey/pnp

  Lecture notes for a short course on proving/programming in Coq via SSReflect.

  Language:Coq16118

• kino3/Mini-TT

  mirror of A simple type-theoretic language: Mini-TT

  Language:Haskell386

• krtx/agda-handson

  agda handson

  Language:Agda63

• mit-plv/bedrock2

  A work-in-progress language and compiler for verified low-level programming

  Language:Coq30045

• qnighy/logic-solver-rs

  Language:Rust453

• vrahli/NuprlInCoq

  Implementation of Nuprl's type theory in Coq

  Language:Coq453

• RedPRL/sml-redprl

  The People's Refinement Logic

  Language:Standard ML22818

• RedPRL/redtt

  "Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

  Language:OCaml20412

• JetBrains/intellij-arend

  Arend plugin for IntelliJ IDEA

  Language:Kotlin9112

• GrammaticalFramework/gf-core

  Grammatical Framework core: compiler, shell & runtimes

  Language:Haskell13436

• haskell/criterion

  A powerful but simple library for measuring the performance of Haskell code.

  Language:Haskell50686

• kcsmnt0/quotient

  quotient types in cubical Agda

  Language:Agda22

• JetBrains/Arend

  The Arend Proof Assistant

  Language:Java70433

• ekmett/linear-haskell

  linear haskell playground

  Language:Haskell112

• mietek/research

  Work in progress

  Language:Agda34

• acorrenson/SATurne

  Tiny verified SAT-solver

  Language:Coq273

• rocq-archive/propcalc

  Propositional Calculus

  Language:Coq6

• andreasabel/miniagda

  A prototypical dependently typed languages with sized types and variances

  Language:Haskell1044

• proofcert/fpc-elpi

  Language:AMPL5

• HoTT/book

  A textbook on informal homotopy type theory

  Language:TeX2k359

• peterlefanulumsdaine/general-type-theories

  A (formalised) general definition of type theories

  Language:Coq572