gmalecha/coq-mod-reduce

Stars
1
Language
OCaml
License
MIT License
Created almost 9 years ago
Updated almost 9 years ago

gmalecha/coq-mod-reduce

gmalecha

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

Modular reduction specifications for cbv

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-refinement

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

coq-seal

Implementation of sealing in Coq with macros for generation

ppx_rewriter

An OCaml optimizer using ppx extensions

categorical-unification

Exploration of unification on categorical terms.