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
0 answers
197 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 ...
Gurkenglas's user avatar
  • 3,714
4 votes
0 answers
200 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 ...
Carl Patenaude Poulin's user avatar
7 votes
1 answer
426 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 ...
Greg Nisbet's user avatar