awesome-provable

A curated set of links to formal methods involving provable code.

GitHub
193 stars
10 watching
8 forks
last commit: almost 3 years ago
Linked from 2 awesome lists

agdacertified-programmingcoqformal-verificationidrisisabelleisabelle-holsel4

Provably Awesome. / Languages
Idris docs
Idris tutorial
Theorem proving with Idris tutorial
Agda Github 2,477 4 days ago
Agda User Manual

Provably Awesome. / Proof Assistants
Coq : Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. [ ] [ ]

Provably Awesome. / Proof Assistants / Coq
https://github.com/Ptival/PeaCoq 106 about 3 years ago
https://math-comp.github.io/mcb/

Provably Awesome. / Proof Assistants
Isabelle : Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. [ ]
HOL : The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. [ ]
LEAN : Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains
K Framework : The K framework is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions or call/cc

Provably Awesome. / Proof Assistants / K Framework
K Tutorial by ,
https://runtimeverification.com/ ( ) : Company formed from K Framework people. Runtime Verification Inc. is currently developing three core products:

Provably Awesome. / Proof Assistants
Viper : Viper (Verification Infrastructure for Permission-based Reasoning) is a language and suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages via translations into the Viper language. ETH Zurich has built several verifiers on top of Viper, including the verifier for Go, for Python and for Rust

Provably Awesome. / Books
Vol. 1:

Backlinks from these awesome lists: