Pinned Repositories
bedrock-mirror-shard
Port of Bedrock to use MirrorShard library for computational reflection
coq-extensible-records
Implementation of extensible records in 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-printf
Implementation of sprintf for Coq
coq-smt-check
Invoke SMT solvers from Coq to check obligations
mirror-core
A framework for extensible, reflective decision procedures.
mirror-shard
Reflective verification procedures for separation logic programs in Coq
skip-list
Pure skip lists in Haskell
template-coq
Reflection library for Coq
gmalecha's Repositories
gmalecha/mirror-shard
Reflective verification procedures for separation logic programs in Coq
gmalecha/bedrock-mirror-shard
Port of Bedrock to use MirrorShard library for computational reflection
gmalecha/coq-plugin-template
Template for Coq plugins
gmalecha/coq-markov
Exploring probabilistic programming in Coq
gmalecha/coq-temporal
An implementation of temporal logic in Coq using Charge!
gmalecha/coq-simulink
Simulink-like formalism in Coq
gmalecha/semantic-query
Semantic query optimization
gmalecha/categorical-unification
Exploration of unification on categorical terms.
gmalecha/coq-mod-reduce
Modular reduction specifications for cbv
gmalecha/coq-refinement
Relational refinements in Coq based on the work of Maxime Denes.
gmalecha/opam-coq-repo
gmalecha/ppx_rewriter
An OCaml optimizer using ppx extensions
gmalecha/Charge
Higher-order separation logic framework in Coq
gmalecha/ChargeCore
gmalecha/compdata
Haskell library implementing "Data Types a la Carte"
gmalecha/coq-checkless
Coq plugin for refine which does not perform type checking.
gmalecha/coq-gc
Coq plugin to force garbage collection
gmalecha/coq-interact
programmatic interaction with coq
gmalecha/coq-universes
gmalecha/HL-Compiler
gmalecha/loop-to-sat
Solve instances of the loop game by converting them to SAT formulas.
gmalecha/mfix
Monadic Fixpoint operations
gmalecha/mtac-plugin
Plugin for Coq 8.5
gmalecha/ocaml-websocket
Websocket library for Lwt
gmalecha/refl-symexec
Reflective symbolic execution
gmalecha/servo
The Servo Browser Engine
gmalecha/smtlib2polya
gmalecha/sparse-memo-trie
Sparse memo tries for more efficient memoization
gmalecha/Synthesis
gmalecha/Timing-plugin
A Coq plugin that allows a user to start and stop timers.