pedrotst

pedrotst's Stars

• typst/typst

  A new markup-based typesetting system that is powerful and easy to learn.

  Language:Rust34.7k922.6k926

• dvanoni/notero

  A Zotero plugin for syncing items and notes into Notion

  Language:TypeScript2.4k26252104

• magmide/magmide

  A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

  Language:Coq812511813

• coq-community/vscoq

  A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]

  Language:OCaml3341441768

• flatangle/flatlib

  Python library for Traditional Astrology

  Language:Python2963781105

• vprover/vampire

  The Vampire Theorem Prover

  Language:C++2952315151

• Deducteam/lambdapi

  Proof assistant based on the λΠ-calculus modulo rewriting

  Language:OCaml2711452835

• RedPRL/cooltt

  😎TT

  Language:OCaml2181914316

• CMU-HoTT/scott

  Selected Papers of Dana S. Scott

  1551316

• coq/opam

  Archive for all Coq related OPAM packages organized in various repositories

  Language:OCaml12319130165

• plclub/metalib

  The Penn Locally Nameless Metatheory Library

  Language:Coq7117823

• bzhan/holpy

  Implementation of higher-order logic in Python

  Language:SMT57406

• granule-project/gerty

  A small implementation of graded modal dependent type theory. A younger cousin to Granule.

  Language:Haskell521121

• yeah-tiger/yeah-tiger.github.io

  :alarm_clock: PL conference deadline countdowns

  Language:HTML52502

• mit-plv/rupicola

  Gallina to Bedrock2 compilation toolkit

  Language:Coq5016911

• wilbowma/mttex

  A LaTeX package for formatting meta-theory.

  Language:TeX465404

• coq-community/paramcoq

  Coq plugin for parametricity [maintainer=@proux01]

  Language:Coq44122224

• tchajed/ltac2-tutorial

  Ltac2 tutorial

  Language:Coq41803

• kyouko-taiga/mvs-calculus

  Compiler for Swiftlet

  Language:Swift34312

• pedrotst/coquedille

  A Coq to Cedille compiler written in Coq

  Language:Coq336332

• RedPRL/algaett

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

  Language:OCaml327150

• impermeable/coq-waterproof

  The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.

  Language:Coq30359

• eduxstad/boiler-grades

  code and data for https://boilergrades.com

  Language:Vue25362

• CoqHott/Program-translations-CC-omega

  Language:Coq13601

• loic-p/PhD-thesis

  My PhD thesis.

  Language:TeX12200

• formal-land/coq-of-ts

  Formal verification for TypeScript

  Language:TypeScript11100

• cedille/cedille2

  Language:Rust9301

• ccyip/coq-idt

  Inductive definition transformers

  Language:Coq42

• mstewartgallus/doublecatrel

  Language:TeX3100

• unboxedtype/EVF

  Everscale Verification Framework

  Language:Dafny1100