152 Open source projects that are alternatives of or similar to Pornview

Mathematical Components

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Automation for de Bruijn syntax and substitution in Coq

Formal Reasoning About Programs

Ltac2 tutorial

Combinatorial species in HoTT

An introductory course to Homotopy Type Theory

A Hello World program in Coq.

A proof of Abel-Ruffini theorem.

Certified Relational to Imperative

Cosette is an automated SQL solver.

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.

This repo is the new home of Proof General

Implementation of sprintf for Coq

Tricks you wish the Coq manual told you

CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)

A gently curated list of companies using verification formal methods in industry

Coq plugin for parametricity [[email protected]]

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

KCoFI Pudding: The formal proofs for the KCoFI system

《软件基础》中译版 Software Foundations Chinese Translation

A Coq library providing tactics to deal with hypothesis

Formalisation of the linear lambda calculus in Coq

A framework for formally verifying distributed systems implementations in Coq

Homotopy type theory

A port of Coq to Javascript -- Run Coq in your Browser

Coq code accompanying several articles on semantics of functional programming languages

Cryptographic Primitive Code Generation by Fiat

The CompCert formally-verified C compiler

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.

An introductory tutorial for the Coq proof assistant.

A Coq IDE build on top of Proof General's Coq mode

Verified vector clocks, with Coq!

Convert Haskell source code to Coq source code

Formalization of C++ for verification purposes.

Verified Software Toolchain

A Certified Interpreter for ML with Structural Polymorphism

IO for Gallina

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

Formal verification of OCaml programs

A Coq library for extensional finite sets and comprehension

Finite sets, finite maps, multisets and generic sets

Implementation of Nuprl's type theory in Coq

Mtac in Agda

Coq proofs of exercises in Pierce's book

Multinomials for the Mathematical Components library.

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

A framework for implementing and certifying impure computations in Coq

Total Parser Combinators in Coq

Bidirectional programming in Haskell with monadic profunctors

Coq executable semantics and resource verifier

An axiom-free formalization of category theory in Coq for personal study and practical work