Programming Languages
22,586 items in 77 lists
-
lambda-rust gitlab.mpi-sws.org
Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.
-
Prosa gitlab.mpi-sws.org
Definitions and proofs for real-time system schedulability analysis.
-
Gappa gitlab.inria.fr
Tactic for discharging goals about floating-point arithmetic and round-off errors.
-
Flocq gitlab.inria.fr
Formalization of floating-point numbers and computations.
-
Itauto gitlab.inria.fr
SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.
-
Coquelicot gitlab.inria.fr
Formalization of classical real analysis compatible with the standard library and focusing on usability.
-
CoqInterval gitlab.inria.fr
Tactics for performing proofs of inequalities on expressions of real numbers.
-
CFML gitlab.inria.fr
Tool for proving properties of OCaml programs in separation logic.
-
Incremental Cycles gitlab.inria.fr
Verified OCaml implementation of an algorithm for incremental cycle detection in graphs.
-
Introduction to the Theory of Computation gitlab.com
Formalization to support an undergraduate course on the theory of computation, including languages and Turing machines.
-
Mathematical Components wiki github.com
-
Docker-Coq GitHub Action github.com
GitHub container action that can be used with Docker-Coq or Docker-MathComp.
-
proof-using-helper.py github.com
Modifies source files to include proof annotations for faster parallel proving.
-
move-vernaculars.py github.com
Lifts many vernacular commands and inner lemmas out of proof script blocks.
-
move-requires.py github.com
Moves all dependency loading statements to the top of source files.
-
minimize-requires.py github.com
Removes loading of unused dependencies.
-
inline-imports.py github.com
Creates stand-alone source files from developments by inlining the loading of all dependencies.
-
find-bug.py github.com
Automatically minimizes source files producing an error, creating small test cases for Coq bugs.
-
absolutize-imports.py github.com
Processes source files to make loading of dependencies robust against shadowing of file names.
-
Official Coq wiki github.com
-
VsCoq Legacy github.com
Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.
-
Dune dune.build
Composable and opinionated build system for OCaml and Coq (former jbuilder).
-
Coq tag on Theoretical Computer Science Stack Exchange cstheory.stackexchange.com
-
Program Logics for Certified Compilers cs.princeton.edu
Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.
-
Official Coq Zulip chat coq.zulipchat.com
-
Planet Coq link aggregator coq.pl-a.net
-
Official Coq standard library coq.inria.fr
-
coqdoc coq.inria.fr
Standard documentation tool that generates LaTeX or HTML files from Coq code.
-
Ltac2 coq.inria.fr
Experimental typed tactic language similar to Coq's classic Ltac language.
-
coq_makefile coq.inria.fr
Build tool distributed with Coq and based on generating a makefile.
-
CoqIDE coq.inria.fr
Standalone graphical tool for interacting with Coq.
-
Official Coq manual coq.inria.fr
-
Coq Package Index coq.inria.fr
Collection of Coq packages based on opam.
-
Coq Zulip chat archive coq.gitlab.io
-
Official Coq Discourse forum coq.discourse.group
-
Tactician coq-tactician.github.io
Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.
-
Coq Tactics in Plain English charlesaverill.github.io
Guide to Coq tactics with explanations and examples.
-
Foundations of Separation Logic chargueraud.org
Introduction to using separation logic to reason about sequential imperative programs in Coq.
-
Coq in a Hurry cel.archives-ouvertes.fr
Introduction to how Coq can be used to define logical concepts and functions and reason about them.
-
Lysxia's blog blog.poisson.chat
-
Certified Programming with Dependent Types adam.chlipala.net
Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
-
Move and Sui with Sam Blackshear from Mysten Labs zeroknowledge.fm
-
Move AMA covering Move origin story twitter.com
-
-
Move and SmartContract Development starcoinorg.github.io
Maintained by the Starcoin team.
-
The Move Prover research.facebook.com
-
Exact and Linear-Time Gas-Cost Analysis research.facebook.com
-
Move IntelliJ plugin plugins.jetbrains.com
Maintained by the Pontem team (source code).
-
Move Playground playground.pontem.network
Like Remix for Move. Alpha version of a Web IDE. See instructions. Maintained by the Pontem team.
-
Movey movey.net
A crates.io-style repository of Move packages.
- next page of items loading…
