Coqrel: binary logical relations for Coq

Introduction

Coqrel is a library for the Coq proof assistant which mechanizes techniques associated with binary logical relations. It provides a unified syntax and methodology for building relations between complex objects, and an extensible tactic library for solving relational goals.

Download

The code is available on github. Beware: Coqrel is a work in progress, and its exact interface has not been finalized yet. With your help and feedback, I will do my best to make it as usable as possible, but I make no promise to preserve backward compatibility until I release the first stable version.

Documentation

I presented Coqrel at the CoqPL'16 workshop; an extended abstract is available which provides a good high-level overview. The following paper may be philosophically useful as well: Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming languages by C. Hermida, U. S. Reddy and E. P. Robinson. WACT 2013.

While documentation is scarce, the code is well-commented and should be readable. You can browse the Coqdoc table of contents and index here. The top-level file LogicalRelations is a good place to start. Coqrel uses typeclasses extensively, both to make the system extensible by the user, and to enable full backtracking between the different components. As a result, some familiarity with the typeclass system of Coq will be valuable to understand the code.

Contact

I encourage you to use github's issue tracker to report any problems you encounter with Coqrel or suggest improvements. For general questions you can also email me directly at jeremie.koenig@yale.edu; I'm always happy to hear from potential users of Coqrel!

-- Jérémie Koenig