Hi,

Is the notion of signature present in OCaml also implemented in Coq?

@MMY MMY yes, see Module Type. (but is that related to this thread?)

Thank you. Sorry, I didn't understand your question. Don't we ask here all the questions relating to the Coq?

@MMY MMY you're adding your question to a Zulip thread about another question

I changed the topic.

@Paolo Giarrusso feel free to edit topics on your own when you see something like this

@Paolo Giarrusso sorry .

I started to learn Coq and I don't understand OCaml very well.

but a code that interests me is written in OCaml and I want to transform it into Coq . Could you give me your opinion on this transformation.

OCaml :

type 'a cont

val callcc: ('a cont -> 'a) -> 'a

val throw: 'a cont -> 'a -> 'b

Coq :

Set Nested Proofs Allowed.

Variable cont : forall (a : Set), Set.

Definition callcc : forall {a : Set}, (cont a -> a) -> a.

Definition throw : forall {a b : Set}, cont a -> a -> b.

That looks almost right but those are the wrong keywords.

```
Module Type MySig.
Parameter cont : forall (a : Type), Type.
Parameter callcc : forall (a : Type), (cont a -> a) -> a.
Parameter throw : forall (a b : Type), cont a -> a -> b.
End MySig.
```

Thank you for your reply.

If I understand correctly if I want to run a test like:

Eval compute in (1 + callcc (fun k => 2 + throw k 3)).

I have to go through another statement:

Modulus M<:MySig.

....

End M.

Do you have specific documentation (course, example, etc.) allowing me to launch my test?

There is a list of introductory materials to learn Coq here https://coq.inria.fr/documentation

Note that module signatures are not at all as necessary as they are in OCaml. Unless you are specifically interested in modules, you can do without. There is also an issue that `throw`

cannot be implemented because Coq is a total language, but you have to walk before you run.

I am no more interested in modules than in transforming this code into Coq, which is why at the start I translated instruction by instruction.

For the rooster courses I followed a lot from start to finish to work with this particular code.

If you can offer me a track to make this code work I will be very grateful.

Why do you want to translate this code into Coq?

Translating impure languages in Coq is a very broad topic, and especially for features like continuations, there are no straightforward answers. So you might want to reassess what it is that you are trying to do to better focus your research.

I want to do the same continuation function in Coq.

Last updated: Apr 14 2024 at 11:02 UTC