GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → DeepSpec → Interactiontrees

DeepSpec / Interactiontrees

Licence: mit
A Library for Representing Recursive and Impure Programs in Coq

Labels

coq

Projects that are alternatives of or similar to Interactiontrees

Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (-36.09%)
Mutual labels:  coq
Coq Ext Lib
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Stars: ✭ 102 (-23.31%)
Mutual labels:  coq
Iron
Coq formalizations of functional languages.
Stars: ✭ 114 (-14.29%)
Mutual labels:  coq
Vscoq
Coq Support for Visual Studio Code
Stars: ✭ 85 (-36.09%)
Mutual labels:  coq
Peacoq
PeaCoq is a pretty Coq, isn't it?
Stars: ✭ 99 (-25.56%)
Mutual labels:  coq
Ceramist
Verified hash-based AMQ structures in Coq
Stars: ✭ 107 (-19.55%)
Mutual labels:  coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-44.36%)
Mutual labels:  coq
Geocoq
A formalization of geometry in Coq based on Tarski's axiom system
Stars: ✭ 128 (-3.76%)
Mutual labels:  coq
Coq Pipes
Stars: ✭ 101 (-24.06%)
Mutual labels:  coq
Awesome Provable
A curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-16.54%)
Mutual labels:  coq
Fourcolor
Formal proof of the Four Color Theorem
Stars: ✭ 87 (-34.59%)
Mutual labels:  coq
Ttlite
A SuperCompiler for Martin-Löf's Type Theory
Stars: ✭ 94 (-29.32%)
Mutual labels:  coq
Ergo
The Language for Smart Legal Contracts
Stars: ✭ 108 (-18.8%)
Mutual labels:  coq
Typetheory
The mathematical study of type theories, in univalent foundations
Stars: ✭ 86 (-35.34%)
Mutual labels:  coq
Coq Of Ocaml
Import OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-12.03%)
Mutual labels:  coq
Ch2o
Stars: ✭ 75 (-43.61%)
Mutual labels:  coq
Mindless Coding
Mindless, verified (erasably) coding using dependent types
Stars: ✭ 104 (-21.8%)
Mutual labels:  coq
Dot
formalization of the Dependent Object Types (DOT) calculus
Stars: ✭ 132 (-0.75%)
Mutual labels:  coq
Fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-10.53%)
Mutual labels:  coq
Coqtail
Interactive Coq Proofs in Vim
Stars: ✭ 109 (-18.05%)
Mutual labels:  coq
View All Similar Projects ➔

Interaction Trees Build Status

A Library for Representing Recursive and Impure Programs in Coq

Introduction

For a quick overview of the core features of the library, see examples/ReadmeExample.v.

See also the tutorial.

The coqdoc documentation for this library is available here.

Top-level modules

  • ITree.ITree: Definitions to program with interaction trees.
  • ITree.ITreeFacts: Theorems to reason about interaction trees.
  • ITree.Events: Some standard event types.

Installation

Via opam

opam install coq-itree

Dependencies

See coq-itree.opam for version details.

Axioms

This library depends on UIP for the inversion lemma:

Lemma eqit_inv_Vis
  : eutt eq (Vis e k1) (Vis e k2) ->
    forall x, eutt eq (k1 x) (k2 x).

There are a few more lemmas that depend on it, but you might not actually need it. For example, the compiler proof in tutorial doesn't need it and is axiom-free.

That lemma also has a weaker, but axiom-free version using heterogeneous equality: eqit_inv_Vis_weak.

The library exports the following axiom for convenience, though it's unlikely you'll need it, and the rest of the library does not depend on it:

Axiom bisimulation_is_eq : t1 ≅ t2 -> t1 = t2.

Contributions welcome

Feel free to open an issue or a pull request!

See also DEV.md for working on this library.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].