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-core
A framework for extensible, reflective decision procedures.
gmalecha/coq-printf
Implementation of sprintf for Coq
gmalecha/coq-interaction-trees
Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.
gmalecha/coq-ltac-iter
Access hint databases from tactics.
gmalecha/template-coq
Reflection library for Coq
gmalecha/coq-smt-check
Invoke SMT solvers from Coq to check obligations
gmalecha/skip-list
Pure skip lists in Haskell
gmalecha/coq-extensible-records
Implementation of extensible records in Coq
gmalecha/coq-plugin-utils
Useful utility functions for writing Coq plugins
gmalecha/coq-k
Some formalization of the K framework in Coq
gmalecha/coq-apply-any
An extension to eauto that allows you to apply an arbitrary lemma from a hint database
gmalecha/coq-seal
Implementation of sealing in Coq with macros for generation
gmalecha/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
gmalecha/bbv
Bedrock Bit Vector Library
gmalecha/category-theory
A formalization of category theory in Coq for personal study and practical work
gmalecha/ceps
Coq Enhancement Proposals
gmalecha/clang
Mirror of official clang git repository located at http://llvm.org/git/clang. Updated every five minutes.
gmalecha/coq
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.
gmalecha/CTRex-aeson.hs
Aeson instances for CTRex records
gmalecha/CTRex.hs
Open records for Haskell
gmalecha/fraxl
gmalecha/gmalecha.github.io
website
gmalecha/Haskell-Foldl-Library
Composable, streaming, and efficient left folds
gmalecha/InteractionTrees
Formalization of the Interaction Tree Datatype in Coq
gmalecha/llvm-project
The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at http://reviews.llvm.org.
gmalecha/metaprogramming-rosetta-stone
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
gmalecha/nixos-weekly
NixOS Weekly Newsletter
gmalecha/rouge
A pure-ruby code highlighter that is compatible with pygments http://rouge.jneen.net/
gmalecha/row-types
gmalecha/SquiggleEq