We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [coq]

Coq is a formal proof management system and semi-interactive theorem prover. Coq is used for the certification of programming language certifications, the formalization of mathematical theorems, teaching, and more.

Filter by
Sorted by
Tagged with
5
votes
0answers
151 views

Prisoner's dilemma with Provability Logic

I am hoping to look at all the possible bots to submit to a noniterated prisoner's dilemma where both bots can reason about each other's behavior. Can I hide ...
4
votes
0answers
155 views

Co-inductive hypothesis for transitivity of stream bisimulation

Catalin Hritcu published some notes on coinduction in Coq, including a discussion of coinduction principles in the style of Giménez and Castéran. One of the exercises is to show that stream ...
6
votes
1answer
199 views

Coq proof that type isomorphism relationship is transitive

The following code is in Coq, a proof assistant by INRIA implemented in OCaml. I'm defining two types as being isomorphic when there exists two functions ...