gmalecha/coq-refinement

Stars
1
Language Coq
Created over 10 years ago
Updated over 9 years ago

gmalecha/coq-refinement

gmalecha

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Relational refinements in Coq based on the work of Maxime Denes.

mirror-core

A framework for extensible, reflective decision procedures.

coq-printf

Implementation of sprintf for Coq

coq-interaction-trees

Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.

coq-ltac-iter

Access hint databases from tactics.

coq-smt-check

Invoke SMT solvers from Coq to check obligations

skip-list

Pure skip lists in Haskell

mirror-shard

Reflective verification procedures for separation logic programs in Coq

coq-extensible-records

Implementation of extensible records in Coq

coq-plugin-template

Template for Coq plugins

bedrock-mirror-shard

Port of Bedrock to use MirrorShard library for computational reflection

coq-temporal

An implementation of temporal logic in Coq using Charge!

coq-plugin-utils

Useful utility functions for writing Coq plugins

coq-markov

Exploring probabilistic programming in Coq

coq-k

Some formalization of the K framework in Coq

coq-simulink

Simulink-like formalism in Coq

semantic-query

Semantic query optimization

coq-apply-any

An extension to eauto that allows you to apply an arbitrary lemma from a hint database

coq-seal

Implementation of sealing in Coq with macros for generation

coq-mod-reduce

Modular reduction specifications for cbv

ppx_rewriter

An OCaml optimizer using ppx extensions

categorical-unification

Exploration of unification on categorical terms.