decrn

decrn's Stars

• decrn/tilogics

  Mechanized proofs and example programs for the paper Type Inference Logics, published at OOPSLA24.

  Language:Coq8

• johnyob/dromedary

  Dromedary is an experimental subset of OCaml, using constraint-based type inference!

  Language:OCaml462

• nachivpn/kripke-style

  Organisation for reading group on Kripke-style semantics

  3

• EmielLanckriet/ASMinCoq

  Language:Coq1

• ztatlock/2024-marktoberdorf-egglog

  Mini egglog in Python

  Language:Python8

• pdfcpu/pdfcpu

  A PDF processor written in Go.

  Language:Go6.9k479

• dafny-lang/dafny

  Dafny is a verification-aware programming language

  Language:C#2.9k262

• art-w/gamelle

  2d game engine for OCaml

  Language:OCaml555

• verifast/verifast

  Research prototype tool for modular formal verification of C and Java programs

  Language:Rust35763

• msp-strath/cs316-functional-programming

  CS316 "Functional Programming" lecture notes

  Language:Haskell146

• oquechy/cfl-reach

  Kotlin implementation of CFL Reachability algorithm for pointer analysis in C++ and Java programs

  2

• kosmikus/lhs2tex

  Preprocessor for typesetting Haskell sources with LaTeX

  Language:Haskell9928

• vellvm/vellvm

  The Vellvm (Verified LLVM) coq development.

  Language:LLVM39734

• acorrenson/metamatix

  A verified implementation of a metamath proof checker

  Language:Coq91

• QGoose/Goose

  An OCaml library for quantum computing

  Language:OCaml10

• acorrenson/minilog

  A verified Implementation of a mini prolog

  Language:Coq131

• coq-community/coq-tricks

  Tricks you wish the Coq manual told you [maintainer=@tchajed]

  Language:Coq49821

• inQWIRE/openqasm-parser

  OCaml library for manipulating OpenQASM Abstract Syntax Tree

  Language:OCaml73

• fmarotta/kaobook

  A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.

  Language:TeX842182

• sweirich/pi-forall

  A demo implementation of a simple dependently-typed language

  Language:Haskell56290

• signalapp/libsignal

  Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.

  Language:Rust3.6k415

• katamaran-project/katamaran

  Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

  Language:Coq174

• fetburner/type-infer

  A Formal Verification of Algorithm W

  Language:Coq17

• kkharji/archive-323

  The neovim language-server-client UI

  Language:Lua41043

• swiftlang/sourcekit-lsp

  Language Server Protocol implementation for Swift and C-based languages

  Language:Swift3.3k276

• sbt/sbt

  sbt, the interactive build tool

  Language:Scala4.8k939

• ilyasergey/pnp

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

  Language:Coq16017

• ekmett/lens

  Lenses, Folds, and Traversals - Join us on web.libera.chat #haskell-lens

  Language:Haskell2k273

• kmonad/kmonad

  An advanced keyboard manager

  Language:Haskell4k321

• scalaz/scalaz

  Principled Functional Programming in Scala

  Language:Scala4.7k710