trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]

LGPL-3.0 License

Stars

18

Committers

View Code on GitHub Visit Website

Ecosystems: Coq

Bot releases are hidden (Show)

trocq - Trocq 0.1.7+prop Latest Release

Published by CohenCyril 3 months ago

This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT.
Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality.

trocq - Trocq 0.1.6

Published by CohenCyril 6 months ago

This is a demo version of Trocq.

trocq - Trocq 0.1.5

Published by CohenCyril 9 months ago

This is a demo version of Trocq.

trocq - Trocq 0.1.4

Published by CohenCyril 9 months ago

This is a demo version of Trocq.

trocq - Trocq 0.1.3

Published by CohenCyril 9 months ago

This is a demo version of Trocq.

trocq - Trocq 0.1.2

Published by ecranceMERCE 9 months ago

trocq - Trocq 0.1.1

Published by CohenCyril 9 months ago

This is a demo version of Trocq.

trocq - Trocq 0.1.0

Published by CohenCyril 9 months ago

This is a demo version of Trocq, compatible with Coq 8.17 with Coq-HoTT and using a custom version of Coq-Elpi.

trocq - ESOP 2024

Published by ecranceMERCE 9 months ago

Artifact for the ESOP 2024 conference

Badges

Extracted from project README's

Related Projects

coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (...

analysis

Mathematical Components compliant Analysis Library

29 Nov 2017 200

paramcoq

Coq plugin for parametricity [maintainer=@proux01]

coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

22 Aug 2012 128

pycoq

Python bindings for the Coq interactive proof assistant

vscoq

Visual Studio Code extension for Coq

10 Jul 2019 335

math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

13 May 2011 160

lemma-overloading

Libraries demonstrating design patterns for programming and proving with canonical structures in ...

PG

This repo is the new home of Proof General

21 Sep 2015 490

PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, doc...

coqtail-math

Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Re...

semantics

A survey of semantics styles in Coq, from natural semantics through structural operational, axiom...

coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]