Categories Alternatives Stacks Self-Hosted Explore

© 2026 Open-Awesome. Curated for the developer elite.

Terms Privacy About GitHub RSS

Program Logics — Coq Formalization of Program Logics | Open Awesome

Home
Coq
Program Logics

Program Logics

Coq

Coq formalization of program logics (Hoare logic, separation logic, concurrent separation logic) for verifying imperative and concurrent programs.

44 stars9 forks0 contributors

Overview

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

Quick Stats

Stars44

Forks9

Contributors0

Open Issues0

Last commit

Related Projects

Community-curated · Updated weekly · 100% open source

Found a gem we're missing?

Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.

Submit a project Star on GitHub

5 years ago

CreatedSince 2021

Tags

#hoare-logic #coq #formal-methods #program-verification #theorem-proving #separation-logic #concurrency-verification #proof-assistant

Built With

Included in

Auto-fetched 1 day ago

Lectures on Software Foundations

Software Foundations

Last commit2 years ago

Mechanized Semantics

Coq development for the course "Mechanized semantics", Collège de France, 2019-2020

Last commit2 years ago

An Introduction to MathComp-Analysis

Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis

Program verification with types and logic

Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen